Opened 3 years ago

Last modified 5 weeks 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.6.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 (13)

comment:1 Changed 3 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 2 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 22 months ago by mpickering

Owner: ssequeira deleted

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

comment:9 Changed 18 months ago by bgamari

Description: modified (diff)
Milestone: 8.0.28.2.1

This won't happen for 8.0.2.

comment:10 Changed 11 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 6 weeks 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 6 weeks 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 5 weeks 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.

Note: See TracTickets for help on using tickets.