[GHC] #14938: Pattern matching on GADT does not refine type family parameters

[GHC]

#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