[GHC] #14938: Pattern matching on GADT does not refine type family parameters
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: GADTs, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Compiling the following code {{{#!hs type family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where R x y Refl = Refl }}} fails with the error {{{#!txt 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 {{{#!hs 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) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by kcsongor): * Attachment "Temp.hs" added. Complete program -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * keywords: GADTs, TypeFamilies => GADTs, TypeFamilies, TypeInType Comment: I agree that talking about `x` and `y` would be an improvement, though I wouldn't call the current message wrong... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by kcsongor): Replying to [comment:1 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 {{{#!idris 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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! :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: | TypeFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14938: Pattern matching on GADT does not refine type family parameters -------------------------------------+------------------------------------- Reporter: kcsongor | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: GADTs, Resolution: invalid | TypeFamilies, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: As stated in comment:6, this is by design, and not a bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14938#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC