#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