[GHC] #12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables)

[GHC]

#12018: Equality constraint not available in pattern type signature
(GADTs/ScopedTypeVariables)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  lowest            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.3
  checker)                           |             Keywords:  GADTs,
      Resolution:                    |  ScopedTypeVariables
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:3 simonpj]:
 > Yes, it is.  The type equalities are available only "after" the match.

 I must admit that I also find this behavior quite counterintuitive. I
 stumbled into this when I tried typechecking this code:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 data family Sing (a :: k)

 data instance Sing (z :: [a]) where
   SNil  :: Sing '[]
   SCons :: Sing x -> Sing xs -> Sing (x ': xs)

 fl :: forall (l :: [a]). Sing l -> Sing l
 fl SNil = SNil
 fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x ': xs)) = SCons x xs
 }}}
 {{{
 GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:17:5: error:
     • Couldn't match type ‘l’ with ‘x : xs’
       ‘l’ is a rigid type variable bound by
         the type signature for:
           fl :: forall a1 (l :: [a1]). Sing l -> Sing l
         at Bug.hs:15:1-41
       Expected type: Sing l
         Actual type: Sing (x : xs)
     • When checking that the pattern signature: Sing (x : xs)
         fits the type of its context: Sing l
       In the pattern:
         SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x : xs)
       In an equation for ‘fl’:
           fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x : xs))
             = SCons x xs
     • Relevant bindings include
         fl :: Sing l -> Sing l (bound at Bug.hs:16:1)
    |
 17 | fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x ': xs)) = SCons x
 xs
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 Bug.hs:17:62: error:
     • Could not deduce: l ~ (x1 : xs1)
       from the context: (x : xs) ~ (x1 : xs1)
         bound by a pattern with constructor:
                    SCons :: forall a (x :: a) (xs :: [a]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘fl’
         at Bug.hs:17:5-39
       ‘l’ is a rigid type variable bound by
         the type signature for:
           fl :: forall a1 (l :: [a1]). Sing l -> Sing l
         at Bug.hs:15:1-41
       Expected type: Sing l
         Actual type: Sing (x : xs)
     • In the expression: SCons x xs
       In an equation for ‘fl’:
           fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x : xs))
             = SCons x xs
     • Relevant bindings include
         xs :: Sing xs (bound at Bug.hs:17:26)
         x :: Sing x (bound at Bug.hs:17:12)
         fl :: Sing l -> Sing l (bound at Bug.hs:16:1)
    |
 17 | fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing (x ': xs)) = SCons x
 xs
    |
 ^^^^^^^^^^
 }}}

 That doesn't typecheck, and yet this does:

 {{{#!hs
 fl :: forall (l :: [a]). Sing l -> Sing l
 fl SNil = SNil
 fl (SCons (x :: Sing x) (xs :: Sing xs) :: Sing l) = SCons x xs
 }}}

 Why not? After all, GHC is smart enough to know how to bind the
 existentially quantified variables `x` and `xs`, so why can't it conclude
 that `l ~ x ': xs` from the GADT pattern match?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12018#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler