#9725: Constraint deduction failure -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by heisenbug): Replying to [comment:11 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
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler