[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 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