Heterogeneous type equality evidence ignored
Either that or I am missing something...
Consider the following,
{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
TypeOperators, ViewPatterns #-}
module Test where
data TypeRep (a :: k) where
TypeCon :: String -> TypeRep a
TypeApp :: TypeRep f -> TypeRep x -> TypeRep (f x)
data TypeRepX where
TypeRepX :: TypeRep a -> TypeRepX
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
trArrow :: TypeRep (->)
trArrow = undefined
eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined
pattern TRFun :: forall fun. ()
=> forall arg res. (fun ~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern TRFun arg res <- TypeApp (TypeApp (eqTypeRep trArrow -> Just HRefl) arg) res
buildApp :: TypeRepX -> TypeRepX -> TypeRepX
buildApp (TypeRepX f) (TypeRepX x) =
case typeRepKind f of
TRFun arg _ ->
case eqTypeRep arg x of
Just HRefl ->
TypeRepX $ TypeApp f x
This fails with,
$ ghc Test.hs -fprint-explicit-kinds
[1 of 1] Compiling Test ( Test.hs, Test.o )
Test.hs:38:30: error:
• Expected kind ‘TypeRep (k1 -> res) a’,
but ‘f’ has kind ‘TypeRep k a’
• In the first argument of ‘TypeApp’, namely ‘f’
In the second argument of ‘($)’, namely ‘TypeApp f x’
In the expression: TypeRepX $ TypeApp f x
• Relevant bindings include
arg :: TypeRep * arg (bound at Test.hs:35:11)
That is, the typechecker doesn't believe that f
's type (why is it saying "kind" here?), TypeRep k a
, will unify with TypeRep (k1 -> res) a
, despite the TRFun
pattern match, which should have brought into scope that k ~ (arg -> res)
.
This was tested with a recent snapshot from ghc-8.0
(23baff79).
Am I missing something here or is this a bug?
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |