It seems to me that GHC should be able to ''conclude'' from `f x ~ g y`

#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 dfeuer): Replying to [comment:1 rwbarton]: that `f` and `g` 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 {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 dfeuer): Replying to [comment:3 rwbarton]:

`f` and `g` here are understood to vary over type constructors, not type synonyms or type families.

Oh, I see. That puts a different spin on things. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): 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 [wiki:DependentHaskell]? I suspect not. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 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, 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 goldfire): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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:15 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 :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9725: Constraint deduction failure -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): The comment stream suggests that it should work when we get kind equalities, which we now have. So yes, let's add a test and declare victory! Make sure Lint is happy. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9725: Constraint deduction failure -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T9725 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * testcase: => polykinds/T9725 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler