Equality not used for substitution
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.