Opened 9 months ago

Closed 7 months ago

#14938 closed bug (invalid)

Pattern matching on GADT does not refine type family parameters

Reported by: kcsongor Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.2
Keywords: GADTs, TypeFamilies, TypeInType Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Compiling the following code

type family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where
  R x y Refl = Refl

fails with the error

Temp.hs:49:9: error:
    • Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’
    • In the third argument of ‘R’, namely ‘Refl’
      In the type family declaration for ‘R’
   |
49 |   R x y Refl = Refl
   |         ^^^^

where Refl is defined as

data a :~: b where
  Refl :: a :~: a

I would expect pattern-matching on Refl to bring the equality x ~ y into scope. It seems like it not only doesn't do that, but the pattern match itself is rejected.

(both 8.2.2 and HEAD)

Attachments (1)

Temp.hs (251 bytes) - added by kcsongor 9 months ago.
Complete program

Download all attachments as: .zip

Change History (10)

Changed 9 months ago by kcsongor

Attachment: Temp.hs added

Complete program

comment:1 Changed 9 months ago by goldfire

But if you have a type-level Refl here, then x and y really will be the same. The equation you want is R x x Refl = Refl, like in those other dependently typed languages. If you write a larger example, I can show you how the equation I suggest will work.

comment:2 Changed 9 months ago by RyanGlScott

I'd be OK with requiring the user write R x x Refl. But in that case, the error message is pretty darn misleading. It's complaining about Refl, but the real error is due to the fact that x and y are distinct, right?

comment:3 Changed 9 months ago by goldfire

Keywords: TypeInType added

I agree that talking about x and y would be an improvement, though I wouldn't call the current message wrong...

comment:4 in reply to:  1 Changed 9 months ago by kcsongor

Replying to goldfire:

But if you have a type-level Refl here, then x and y really will be the same. The equation you want is R x x Refl = Refl, like in those other dependently typed languages.

In the end I did end up using that equation, but my original idea was to try and avoid non-linear patterns, and passing in an explicit proof seemed like a sensible idea. For example, Idris lets me write

r : x -> y -> x = y -> x = y
r x y Refl = Refl

(But of course non-linear patterns are not supported)

Is there something obvious I missed that would explain why this form of matching should not accepted?

comment:5 Changed 9 months ago by goldfire

Hm. Maybe it's only Agda that requires you to write a non-linear pattern here. Except that the pattern isn't really non-linear, because the non-linearity (at least in Agda) isn't checked. (Agda has a notation for an argument that has to be a certain way but that isn't checked for when matching.)

In any case, you're right, though. Refl doesn't bring into scope any coercion. Instead, the appearance of Refl requires a coercion in order for the equation to match. But because type family equations are at the top level and that there is no phase separation between kind-checking and type-checking, this is all OK. After all, the same type checker that allowed Refl to be type checked at the type family application site is checking whether the equation matches; if one can prove the types equal, the other can, too.

This design decision does have a few consequences, though. For example, you can't quantify a type family equation over an equality between type family applications: type family F a (pf :: G a :~: H a). That just won't work (for several reasons). Of course, it's my hope that we won't have type families in a few years and can use normal GADT pattern matching instead! :)

comment:6 Changed 9 months ago by kcsongor

Thanks for the explanation! I have encountered that limitation on several occasions, but it never quite clicked; now it makes total sense. So the only way to match pf against Refl is by first providing an a for which G a and H a can actually reduce to the same thing

type family G a where
  G Int = Nat

type family H a where
  H Int = Nat

type family F a (pf :: G a :~: H a) where
  F Int Refl = True

So it seems like I got the "direction" of the matching wrong. Could you by any chance point me to any resources where this decision is explained in more detail? I skimmed the System FC with Explicit Kind Equality paper, but it wasn't obvious where this would be described.

In any case, I'm happy to close this ticket, as I'm now convinced it's not a bug.

comment:7 Changed 9 months ago by Iceland_jack

Cc: Iceland_jack added

comment:8 Changed 9 months ago by goldfire

No, I can't point you to more discussion -- this was a decision of convenience during implementing. At the time, I hadn't fully noticed all the ramifications of it.

comment:9 Changed 7 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

As stated in comment:6, this is by design, and not a bug.

Note: See TracTickets for help on using tickets.