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

19 Mar 2018

      #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