[GHC] #12919: Equality not used for substitution

[GHC]

#12919: Equality not used for substitution
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:  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:                    |
-------------------------------------+-------------------------------------
Description changed by int-index:

@@ -10,1 +10,1 @@
- data Nat = Z
+ data N = Z
@@ -12,2 +12,2 @@
- data D :: Nat -> Type where
-   DZ :: D Z
+ data V :: N -> Type where
+   VZ :: V Z
@@ -15,1 +15,1 @@
- type family VC (n :: Nat) :: Type where
+ type family VC (n :: N) :: Type where
@@ -18,2 +18,2 @@
- type family VF (xs :: D n) (f :: VC n) :: Type where
-   VF DZ f = f
+ type family VF (xs :: V n) (f :: VC n) :: Type where
+   VF VZ f = f
@@ -24,1 +24,1 @@
- prop :: xs ~ DZ => Dict (VF xs f ~ f)
+ prop :: xs ~ VZ => Dict (VF xs f ~ f)
@@ -31,1 +31,1 @@
- Op.hs:20:8: error:
+ T12919.hs:22:8: error:
@@ -37,1 +37,1 @@
-         at Op.hs:19:9
+         at T12919.hs:21:9
@@ -41,1 +41,1 @@
-         prop :: Dict VF xs f ~ f (bound at Op.hs:20:1)
+         prop :: Dict VF xs f ~ f (bound at T12919.hs:22:1)

New description:

 This code

 {{{
 {-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}

 module T12919 where

 import Data.Kind

 data N = Z

 data V :: N -> Type where
   VZ :: V Z

 type family VC (n :: N) :: Type where
   VC Z = Type

 type family VF (xs :: V n) (f :: VC n) :: Type where
   VF VZ f = f

 data Dict c where
   Dict :: c => Dict c

 prop :: xs ~ VZ => Dict (VF xs f ~ f)
 prop = Dict
 }}}

 fails with this error:

 {{{
 T12919.hs:22:8: error:
     • Couldn't match type ‘f’ with ‘VF 'VZ f’
         arising from a use of ‘Dict’
       ‘f’ is a rigid type variable bound by
         the type signature for:
           prop :: forall (xs :: V 'Z) f. xs ~ 'VZ => Dict VF xs f ~ f
         at T12919.hs:21:9
     • In the expression: Dict
       In an equation for ‘prop’: prop = Dict
     • Relevant bindings include
         prop :: Dict VF xs f ~ f (bound at T12919.hs:22:1)
 }}}

 However, if I substitute `xs` with `VZ` (by hand) in the type of `prop`,
 it compiles. Can be reproduced with GHC 8.0.1 but not HEAD.

--

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