Opened 3 years ago

Last modified 3 months ago

#10789 new feature request

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

Reported by: goldfire Owned by: v0d1ch
Priority: normal Milestone: 8.8.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: #13192 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 (20)

comment:1 Changed 3 years ago by goldfire

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

comment:2 Changed 3 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 3 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:4 Changed 3 years ago by ssequeira

Milestone: 8.0.1
Owner: set to ssequeira

comment:5 Changed 3 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 3 years ago by thomie

Keywords: TypeFamilies added

comment:7 Changed 2 years 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 2 years ago by mpickering

Owner: ssequeira deleted

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

comment:9 Changed 2 years ago by bgamari

Description: modified (diff)
Milestone: 8.0.28.2.1

This won't happen for 8.0.2.

comment:10 Changed 18 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

comment:11 Changed 8 months ago by ckoparkar

Hello. I'm a newcomer, and would like to give this a shot. As goldfire suggested, I've started looking at TcErrors.

comment:12 Changed 8 months ago by goldfire

A word of warning: TcErrors bears the accumulation of small patches that have been applied to incrementally improve error messages. I, personally, always find the module hard to navigate. However, if you have a specific erroneous situation in mind, it's not that hard to trace how that particular error filters through the module, and you should be able to find the stretch of code where the error itself is rendered. (A good starting place is to search for the text printed in the current error message.)

To fix this, you'll have to add an extra check somewhere and then tailor the error message if necessary.

Give a holler if you get stuck!

comment:13 Changed 8 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:14 Changed 4 months ago by RyanGlScott

comment:15 Changed 4 months ago by v0d1ch

Hey @ckoparkar do you still work on this ?

comment:16 Changed 4 months ago by v0d1ch

Owner: set to v0d1ch

comment:17 Changed 3 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for 8.6, bumping to 8.8.

comment:18 Changed 3 months ago by simonpj

Sasa asks (on ghc-devs)

With the help of @int_index I found the place in TcErrors.hs where the error printing occurs and I think the check that I need to add will look similar to this one https://github.com/ghc/ghc/blob/master/compiler/typecheck/TcErrors.hs#L1935.

So I guess that we need to check if one of the kinds of two types we are comparing defaults to * (or Type if you will) and then add new warning that will be more descriptive as to why the failure happened. Maybe there is a way to check if what we are comparing are actually type families so that would make the job easier I guess.

Richard replies

I don't think the problem is particular to Type or defaulting. Instead, the problem is when

  • one of the two mismatched types is a type family application
  • and the type family has equations that pattern-match on an invisible parameter,
  • and it's that invisible-parameter matching that's gone awry.

Now that I think about it, detecting these particular conditions might be tricky: you might need to edit code in FamInstEnv that does type family equation lookup to return diagnostic information if a match fails. (I would look at reduceTyFamApp_maybe, and perhaps it can return something more interesting than Nothing in the failure case.)

comment:19 Changed 3 months ago by v0d1ch

I have determined that in the failure case in this specific example we want the Role to be Nominal and we get a [Type] that looks like this:

[* -> *, Maybe]

while the TyCon is F

How would I proceed further with these informations ?

I am also wondering if I should introduce new type that will give us the option to customize failure message instead of just Nothing ?

Last edited 3 months ago by v0d1ch (previous) (diff)

comment:20 in reply to:  19 Changed 3 months ago by goldfire

How would I proceed further with these informations ?

Not quite sure how to answer this. You might need to continue tracing the code path into tcMatchTys.

I am also wondering if I should introduce new type that will give us the option to customize failure message instead of just Nothing ?

Yes, I think so. For example, instead of Nothing, maybe it would work well to return an Int that gives the index of the first argument that mismatches. Then, the error-message generator could see if that index corresponds to an invisible argument; if so, suggest -fprint-explicit-kinds. Perhaps there's a better design, as well.

Note: See TracTickets for help on using tickets.