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

Bug.hs:14:7:
    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: 7.12.18.0.1

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

Milestone: 8.0.18.0.2

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)
Milestone: 8.0.28.2.1

This won't happen for 8.0.2.

comment:10 Changed 8 months ago by bgamari

Milestone: 8.2.18.4.1

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.