Opened 3 years ago

Closed 7 weeks ago

Last modified 7 weeks ago

#9725 closed bug (fixed)

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: polykinds/T9725
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)

9725.hs (1.5 KB) - added by heisenbug 3 years ago.
Simplified reproduction testcase
9725-RAE.hs (2.0 KB) - added by goldfire 3 years ago.
9725-GGR.hs (1.6 KB) - added by heisenbug 3 years ago.
Now with a new (T i) type in kind En
9725-GGR.2.hs (1.6 KB) - added by heisenbug 3 years ago.
Getting rid of Proxy in Hi (exploiting the characteristics of the bug at hand)

Download all attachments as: .zip

Change History (25)

comment:1 Changed 3 years ago by rwbarton

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 into f ~ g, x ~ y unless it knows already that f and g (or equivalently x and y) have the same kind.

It seems to me that GHC should be able to conclude from f x ~ g y 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?

comment:2 in reply to:  1 Changed 3 years ago by dfeuer

Replying to rwbarton:

It seems to me that GHC should be able to conclude from f x ~ g y 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

{-# 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 Changed 3 years ago by rwbarton

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

comment:4 in reply to:  3 Changed 3 years ago by dfeuer

Replying to 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.

comment:5 in reply to:  1 Changed 3 years ago by heisenbug

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.

Changed 3 years ago by heisenbug

Attachment: 9725.hs added

Simplified reproduction testcase

comment:6 Changed 3 years ago 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 DependentHaskell? I suspect not.

Simon

comment:7 in reply to:  6 Changed 3 years ago by heisenbug

Replying to simonpj: ... snip ...

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.

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 Changed 3 years ago 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

comment:9 in reply to:  8 Changed 3 years ago by heisenbug

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, 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).

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 equality k ~ Bool and in others you have k ~ 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 3 years ago 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.

comment:11 Changed 3 years ago by 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, usafeCoerce may be needed.

Simon

comment:12 Changed 3 years ago 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.

comment:13 Changed 3 years ago by goldfire

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 in reply to:  11 Changed 3 years ago by heisenbug

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 Changed 3 years ago by 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.

Changed 3 years ago by goldfire

Attachment: 9725-RAE.hs added

Changed 3 years ago by heisenbug

Attachment: 9725-GGR.hs added

Now with a new (T i) type in kind En

comment:16 in reply to:  15 Changed 3 years ago by heisenbug

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 3 years ago by heisenbug

Attachment: 9725-GGR.2.hs added

Getting rid of Proxy in Hi (exploiting the characteristics of the bug at hand)

comment:17 Changed 7 weeks ago by RyanGlScott

I'm arriving at this bug quite late, but it appears that https://ghc.haskell.org/trac/ghc/attachment/ticket/9725/9725.hs works on GHC 8.0.1 and later without a hitch. Perhaps it's time to consider this bug fixed?

comment:18 Changed 7 weeks ago 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

comment:19 Changed 7 weeks ago by Ryan Scott <ryan.gl.scott@…>

In a02039c/ghc:

Add regression test for #9725

Kind equalities saves the day!

comment:20 Changed 7 weeks ago by RyanGlScott

Resolution: fixed
Status: newclosed
Test Case: polykinds/T9725

comment:21 Changed 7 weeks ago by heisenbug

Thanks to everybody involved!

Note: See TracTickets for help on using tickets.