#11642 closed bug (invalid)
Heterogeneous type equality evidence ignored
Reported by: | bgamari | Owned by: | goldfire |
---|---|---|---|
Priority: | highest | Milestone: | 8.0.1 |
Component: | Compiler (Type checker) | Version: | 7.10.3 |
Keywords: | TypeInType | Cc: | simonpj |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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
(23baff798aca5856650508ad0f7727045efe3680).
Am I missing something here or is this a bug?
Change History (11)
comment:1 Changed 2 years ago by
comment:2 Changed 2 years ago by
The problem isn't actually the pattern synonym at all. Even the straightforward nested-case approach fails in the same way,
buildApp :: TypeRepX -> TypeRepX -> TypeRepX buildApp (TypeRepX f) (TypeRepX x) = case typeRepKind f of TypeApp (TypeApp ty arg) res -> case eqTypeRep trArrow ty of Just HRefl -> case eqTypeRep arg x of Just HRefl -> TypeRepX $ TypeApp f x
comment:4 Changed 2 years ago by
Summary: | Typechecker doesn't use evidence available from pattern synonym? → Heterogeneous type equality evidence ignored |
---|
comment:5 Changed 2 years ago by
Judging by the -ddump-tc-trace
output (for the fully expanded case
version
given in comment:2), the problem is that this wanted is unsolved,
wanted :: (~#) k1 k1 x1 ((TYPE |> <Levity>_N -> Sym cobox_a1Mi) 'Lifted) (CNonCanonical)}
given these givens,
(~#) * * k2 (f1 x2) (~#) (k3 -> *) (k3 -> *) f1 (f2 x1) (~#) * * (* -> * -> *) (k1 -> k3 -> *) (~#) (* -> * -> *) (k1 -> k3 -> *) (->) f2 (~#) * * k1 k4 (~#) k1 k4 x1 a
comment:6 Changed 2 years ago by
Oddly enough, if I ask for the same wanted in a slightly more direct way, things work,
data IsFunc' a b where IsFunc' :: forall x y a b (f :: x -> y). IsFunc' (TypeRep f) (TypeRep x) buildApp :: forall k. forall (a :: k) b. TypeRep a -> TypeRep b -> IsFunc' (TypeRep a) (TypeRep b) buildApp f x = case typeRepKind f of TypeApp (TypeApp ty arg) res -> case eqTypeRep trArrow ty of Just HRefl -> case eqTypeRep arg x of Just HRefl -> IsFunc'
comment:8 Changed 2 years ago by
Keywords: | TypeInType added |
---|
Richard I think this needs your loving care. I had a look but ran out of time in a maze of twisty little casts, all alike.
comment:9 Changed 2 years ago by
Owner: | set to goldfire |
---|
comment:10 Changed 2 years ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
A maze this is, indeed. But, happily(?), we humans were the ones lost, not GHC, which is spot on.
The original code is
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
Let me augment with some kinds and such:
buildApp :: TypeRepX -> TypeRepX -> TypeRepX buildApp (TypeRepX f) (TypeRepX x) = -- f :: TypeRep kind_tf (tf :: kind_tf) -- x :: TypeRep kind_tx (tx :: kind_tx) case typeRepKind f of TRFun arg _ -> -- arg :: TypeRep kind_targ (targ :: kind_targ) -- _ :: TypeRep kind_tres (tres :: kind_tres) -- _ :: kind_tf ~ (targ -> tres) -- _ :: kind_targ ~ * -- _ :: kind_tres ~ * case eqTypeRep arg x of Just HRefl -> -- _ :: kind_targ ~ kind_tx (but kind_targ ~ *) -- _ :: targ ~ tx TypeRepX $ TypeApp f x -- NEED: exists k1 k2. -- kind_tf ~ k1 -> k2 -- kind_tx ~ k1
At the end, we need to find k1
and k2
such that those two equalities are provable from our givens. The choice of k1
and k2
is quite clear: choose k1 := targ
and k2 := tres
. Now, we must prove kind_tx ~ targ
. But we can't! We know that targ ~ tx
, not targ ~ kind_tx
. Note that, actually, kind_tx
is really known to be *
. So GHC helpfully reports
T11642.hs:47:30: error: • Could not deduce: arg ~ * from the context: k ~ (arg -> res) bound by a pattern with pattern synonym: TRFun :: forall fun arg res. (fun ~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun, in a case alternative at T11642.hs:37:5-15 or from: (* ~ k1, arg ~ a1) bound by a pattern with constructor: HRefl :: forall k2 (a :: k2). a :~~: a, in a case alternative at T11642.hs:44:14-18 ‘arg’ is a rigid type variable bound by a pattern with pattern synonym: TRFun :: forall fun arg res. (fun ~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun, in a case alternative at T11642.hs:37:5 Expected type: TypeRep a Actual type: TypeRep 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 T11642.hs:37:11)
Which is absolutely correct.
Happily, fixing the code is easy:
-- ... case eqTypeRep arg (typeRepKind x) of -- ...
works like a charm.
I do believe some intermediate work (between when this was reported and now) has improved this message. It's still not great, given that it took me the better part of an hour to deduce all of the above. But I don't see how we can do better without giving the user the trail of breadcrumbs that GHC used to find its result. (I do think we should give this ability to the user, somehow. It would be easy enough to implement -- just augment CtLoc
to keep track of previous constraints and how they were transformed. The data is all there.)
I'm thus closing this as invalid. I'm also not adding a regression test, because I'm not thrilled with the error message as it is, and there's no other unusual behavior here.
comment:11 Changed 2 years ago by
Oh dear, what a silly mistake on my part. Thanks for tracking this down Richard.
Looks like a bug to me.
Also you're right that the error message should say "type".