Opened 3 years ago
Last modified 2 years ago
#9725 new bug
Constraint deduction failure
Reported by: | heisenbug | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.8.3 |
Keywords: | Cc: | ||
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
I get a strange error message like this
[1 of 1] Compiling Main ( 08-10.hs, interpreted ) 08-10.hs:254:33: Could not deduce (KnownLoc (ent par1 a)) arising from a use of ‘Hidden'’ from the context (List ConfFamily ts) bound by the type signature for locAware :: List ConfFamily ts => (forall (i :: k). KnownLoc (ent par i) => ConfFamily (Facility (ent par i)) ts) -> Con ConfFamily (On ent par) at 08-10.hs:251:13-160 or from (ent par a ~ 'Monitor par1 mp, KnownLoc ('Monitor par1 mp)) bound by a pattern with constructor MonitorF :: forall (par :: Entity) (mp :: MonitorPoint). KnownLoc ('Monitor par mp) => String -> String -> Observer -> Bool -> Facility ('Monitor par mp), in an equation for ‘h’ at 08-10.hs:254:19-28 In the expression: Hidden' (d f) In an equation for ‘h’: h (Hide f@(MonitorF {})) = Hidden' (d f) In an equation for ‘locAware’: locAware descr = Abstr h where h :: (ent `On` par) -> ConfFamily (ent `On` par) ts h (Hide f@(MonitorF {})) = Hidden' (d f) d :: KnownLoc (ent par i) => Facility (ent par i) -> ConfFamily (Facility (ent par i)) ts d _ = descr Failed, modules loaded: none.
I have many language extensions active, such as, DataKinds
, ScopedTypeVariables
, etc.
If somebody says this indeed looks like a bug, then I'll try to post a minimal reproduction case.
My reasoning goes like this
Here are the relevant facts that GHC figured out from a GADT pattern match:
(ent par a ~ 'Monitor par1 mp, KnownLoc ('Monitor par1 mp))
From this I discover these equalities:
ent === 'Monitor (*) par === par1 (**) a === mp (***)
Substituring (*)
^{-1} and (***)
^{-1} into the given KnownLoc ('Monitor par1 mp)
results in the desired KnownLoc (ent par1 a)
Looks like a bug, right?
Attachments (4)
Change History (20)
comment:1 follow-ups: 2 5 Changed 3 years ago by
comment:2 Changed 3 years ago by
Replying to rwbarton:
It seems to me that GHC should be able to conclude from
f x ~ g y
thatf
andg
have the same kind, but maybe it has no way to represent this?I think there is a related Trac ticket also, but I couldn't find it.
Maybe adding kind annotations for some of the type variables involved would help?
I don't know what you're doing, but if I understand what you're getting at, I don't think it's true in general. Consider
{-# LANGUAGE TypeFamilies, TypeOperators, KindSignatures #-} module ConstraintEq where type family Id a :: * where Id x = x type family YaKnow a :: * where YaKnow x = x Int
Here Id Int ~ YaKnow Id
, but Id
and YaKnow
have different kinds.
comment:3 follow-up: 4 Changed 3 years ago by
f
and g
here are understood to vary over type constructors, not type synonyms or type families.
comment:4 Changed 3 years ago by
Replying to rwbarton:
f
andg
here are understood to vary over type constructors, not type synonyms or type families.
Oh, I see. That puts a different spin on things.
comment:5 Changed 3 years ago by
Replying to rwbarton:
...
Maybe adding kind annotations for some of the type variables involved would help?
I tried that. These are the most generic kinds:
ent :: Entity -> k -> Entity Monitor :: Entity -> Bool -> Entity par :: Entity mp :: Bool
It looks like the equation (*)
does not seem to establish the kind-level equality Entity -> k -> Entity === Entity -> Bool -> Entity
and thus k === Bool
. So yes, your analysis is correct, that kind variables mess up the decomposition.
When changing ent
to Monitor
, everything works, probably because the kind variable k
is eliminated.
comment:6 follow-up: 7 Changed 2 years ago by
Richard, why do you think this is a bug?
Looking at the simplified reproduction test case, we see
-- Restricted kind signature: --test :: forall (ent :: Bool -> En) . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) test :: forall ent. (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent)
The program typechecks fine with "restricted kind signature" (agreed?), with GHC 7.8.2 or HEAD. So decomposition of type applications is working fine (i.e. comment:1 is not right; although in previous versions of GHC Reid was correct).
The actual problem is that the type signature (the one not in comments) kind-checks like this:
test :: forall k. forall (ent :: k -> En). (forall (i::k). Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent)
The pattern-match on Mb
indeed yields the given equality ent::k ~ M::Bool
. But we can't use that unless we know that k~Bool
and, until Richard implements kind-level equalities, we don't know that.
The "restricted kind signature" de-polymorphises" it, which is all you need to make it work.
Richard: you should add this to your test suite for kind-level equalities! Is there a wiki page for this? Is it DependentHaskell? I suspect not.
Simon
comment:7 Changed 2 years ago by
Replying to simonpj: ... snip ...
The pattern-match on
Mb
indeed yields the given equalityent::k ~ M::Bool
. But we can't use that unless we know thatk~Bool
and, until Richard implements kind-level equalities, we don't know that.
But isn't this just plain kind inference as we have it today?
The "restricted kind signature" de-polymorphises" it, which is all you need to make it work.
Right, that's what I figured. But in my actual code I have
data En = M Bool | Ind Nat -- etc. data Fac :: En -> * where Mo :: Kn (M b) => Fac (M b) Odu :: Kn (Ind n) => Fac (Ind n) -- etc.
And the pattern match in h
goes over these, so I *need* the poly-kindedness. It would let me consolidate a bunch of otherwise identical functions (modulo constructor names).
Richard: you should add this to your test suite for kind-level equalities! Is there a wiki page for this? Is it DependentHaskell? I suspect not.
Simon
comment:8 follow-up: 9 Changed 2 years ago by
No it's not just kind inference. Do you want that poly-kinded type for test
? Sounds as if the answer is "yes". Well, then k
is a skolem variable, and if it is is locally known to be equal to Bool
, that's a local kind equality (a la GADTs).
From what you say, in some branches of h
, you have a local equality k ~ Bool
and in others you have k ~ Nat
.
This is just what Richard is working on!
Simon
comment:9 Changed 2 years ago by
Replying to simonpj:
No it's not just kind inference. Do you want that poly-kinded type for
test
? Sounds as if the answer is "yes". Well, thenk
is a skolem variable, and if it is is locally known to be equal toBool
, that's a local kind equality (a la GADTs).
While I suspected that this could be the answer, I am still happy I asked! Thanks for explaining.
From what you say, in some branches of
h
, you have a local equalityk ~ Bool
and in others you havek ~ Nat
.
Exactly. k
will be instantiated to different kinds in the pattern matching process.
This is just what Richard is working on!
Good to hear. Is there an ETA for this work? Is there a chance to have a stripped-down version of that feature as a preview, that handles just such plain equations, without the full bells&whistles goodness? Would a plain mortal like me be in a position to make the former happen?
Simon
Thanks again,
Gabor
comment:10 Changed 2 years ago by
But you don't have to decompose the given equality to get the wanted. We have
[G] e1 :: ent k1 ~ M b [G] e2 :: Kn (M b) [W] e3 :: Kn (ent k1)
Solve with
e3 := e2 |> Kn (sym e1)
The problem is that GHC tries to decompose the given, fails utterly, and then has no way forward. So, I'd say this shows a completeness bug in the solver. It's one we may not want to address, as I agree my kind equality stuff makes this straightforward and I don't see an easy way of solving this problem.
comment:11 follow-up: 14 Changed 2 years ago by
Ah I see. You are right. But this is pretty coincidental. If the wanted was [W] ent ~ M
we'd be out of luck. And taking account of the coincidence is far from straightforward; it would be a significant complication in the solver, which will be redundant when your stuff lands.
So I propose to wait. Sorry Gabor, but Richard's stuff is itself a major increment, and I just don't know what a simple cut-down version might look like. ETA is up to Richard. Meanwhile, usafeCoerce
may be needed.
Simon
comment:12 Changed 2 years ago by
ETA on my work is "not 7.10". There are three primary things that my work (for now) addresses: 1) kind equalities in terms, 2) promoted GADTs, and 3) promoted type families. Item (1) feels quite close to start the discussion about merging, maybe a few more weeks. (2) and (3) are in the 2-3 month timeframe, I think. However, I think it's reasonable to consider merging (1) even if (2) and (3) are unfinished. (1) by itself will solve this problem, and the dynApply
problem highlighted in wiki:Typeable.
In any case, my campaign toward merging won't start in earnest until I have something to show that I'm proud of, and that time isn't quite yet.
comment:13 Changed 2 years ago by
Oh -- and I agree with Simon that the fact that this is soluble is a lucky coincidence and not worth fixing right now.
comment:14 Changed 2 years ago by
Replying to simonpj:
Ah I see. You are right. But this is pretty coincidental. If the wanted was
[W] ent ~ M
we'd be out of luck. And taking account of the coincidence is far from straightforward; it would be a significant complication in the solver, which will be redundant when your stuff lands.So I propose to wait. Sorry Gabor, but Richard's stuff is itself a major increment, and I just don't know what a simple cut-down version might look like. ETA is up to Richard. Meanwhile,
unsafeCoerce
may be needed.
I am trying to go the unsafeCoerce
route. But I have not succeeded to write it yet. I keep getting kind mismatch errors in line 27. So I replaced the call to d
there with a hole _
. Then I get this diagnostic:
9725.hs:27:30: Found hole _ with type: Fac (ent k1) -> Fm (Fac (ent b0)) Where: ent is a rigid type variable bound by the type signature for test :: (forall (i :: k). Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:24:16 k1 is a rigid type variable bound by a pattern with constructor Hi :: forall (k :: BOX) (ent :: k -> En) (k :: k). Fac (ent k) -> O ent, in an equation for h at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:27:14 b0 is an ambiguous type variable Relevant bindings include m :: Fac (ent k1) (bound at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:27:17) h :: O ent -> Fm (O ent) (bound at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:27:11) d :: forall (i :: k). Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i)) (bound at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:29:11) de :: forall (i :: k). Kn (ent i) => Fm (Fac (ent i)) (bound at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:25:6) test :: (forall (i :: k). Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) (bound at /home/ggreif/ReleaseFeatureMatrix/bachelor/9725.hs:25:1) In the expression: _ In the first argument of HiF , namely (_ m) In the expression: HiF (_ m) Failed, modules loaded: none.
Stangely the type reported for m
is Fac (ent k1)
(which comes from the context provided by Hi
and not from the context provided by Mo
, which would be Fac (M b)
.
This changes to the expected one with the "restricted" signature. I believe this is the place where the "badness" happens. Does this finding change something w.r.t. the analysis?
Simon
comment:15 follow-up: 16 Changed 2 years ago by
After some struggle, I came up with a working construction, attached. Bonus points if you can make it prettier and/or bind the scoped type variables without adding proxies.
Changed 2 years ago by
Attachment: | 9725-RAE.hs added |
---|
comment:16 Changed 2 years ago by
Replying to goldfire:
After some struggle, I came up with a working construction, attached. Bonus points if you can make it prettier and/or bind the scoped type variables without adding proxies.
Thanks, Richard, this is very cool. It will take a while for me to analyse what exactly you are doing. I attached a version based on your workaround that makes the kind En
a bit more interesting. I believe I can now transfer this into my real code :-)
Changed 2 years ago by
Attachment: | 9725-GGR.2.hs added |
---|
Getting rid of Proxy
in Hi
(exploiting the characteristics of the bug at hand)
The thread starting at http://www.haskell.org/pipermail/glasgow-haskell-users/2013-December/024466.html may be relevant. In short, GHC does not decompose
f x ~ g y
intof ~ g, x ~ y
unless it knows already thatf
andg
(or equivalentlyx
andy
) have the same kind.It seems to me that GHC should be able to conclude from
f x ~ g y
thatf
andg
have the same kind, but maybe it has no way to represent this?I think there is a related Trac ticket also, but I couldn't find it.
Maybe adding kind annotations for some of the type variables involved would help?