Opened 2 years ago

Last modified 8 months ago

#10789 new feature request

Notify user when a kind mismatch holds up a type family reduction

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 7.10.2
Keywords: newcomer, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

Consider this contrived example:

{-# LANGUAGE TypeFamilies, PolyKinds, UndecidableInstances #-}

module Bug where

import Data.Proxy

type family F (a :: k) :: k
type instance F a = G a

type family G a
type instance G a = a

foo :: Proxy (F Maybe) -> Proxy Maybe
foo = id

This (correctly) fails to compile. The error message is

    Couldn't match type ‘F Maybe’ with ‘Maybe’
    Expected type: Proxy (F Maybe) -> Proxy Maybe
      Actual type: Proxy Maybe -> Proxy Maybe
    In the expression: id
    In an equation for ‘foo’: foo = id
Failed, modules loaded: none.

But this is peculiar, but it surely looks like F should be a type-level identity function! Of course, upon further inspection, we see that F is partial. It reduces only at kind *. This is quite hard to figure out, though, especially given that we're using the "default to *" behavior of open type families to arrange for this kind restriction.

Thus, I propose: figure out when a type family reduction is held up due to a kind mismatch, and inform the user.

Change History (10)

comment:1 Changed 2 years ago by goldfire

See also #10775 for the error that originally inspired this request.

comment:2 Changed 2 years ago by goldfire

Keywords: newcomer added
Milestone: 7.12.1

A little coding in TcErrors should do it. Happy to advise someone who wants to take this on.

comment:3 Changed 2 years ago by thoughtpolice


Milestone renamed

comment:4 Changed 2 years ago by ssequeira

Milestone: 8.0.1
Owner: set to ssequeira

comment:5 Changed 2 years ago by goldfire

Milestone: 8.0.1

Thanks, ssequeira!

I assume the change in milestone was accidental, and so I'm reverting it. Setting a milestone to bottom effectively means that we've given up on the ticket.

comment:6 Changed 23 months ago by thomie

Keywords: TypeFamilies added

comment:7 Changed 21 months ago by thoughtpolice


I'm bumping this to 8.0.2 and moving this from the 8.0.1 queue, since it's not critical but would be 'nice to have' for error messages.

comment:8 Changed 20 months ago by mpickering

Owner: ssequeira deleted

Please reassign yourself ssequeira if you are still working on this ticket.

comment:9 Changed 15 months ago by bgamari

Description: modified (diff)

This won't happen for 8.0.2.

comment:10 Changed 8 months ago by bgamari


Given that 8.2.1-rc1 is imminent, I'm bumping these off to the 8.4

Note: See TracTickets for help on using tickets.