Opened 14 months ago

Closed 4 months ago

Last modified 4 months ago

#9103 closed bug (invalid)

hackage's type-level-0.2.4 fails to compile

Reported by: slyfox Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: Cc: dreixel, diatchki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #8634 Differential Revisions:

Description

Attached trimmed-down dependencyless archive.
Steps to reproduce:

$ tar -xzf type-level-0.2.4.tar.gz
$ ghci -hide-all-packages -package=base -package=template-haskell Data/TypeLevel.hs

The error on 7.8.2 and in -HEAD is:

[6 of 8] Compiling Data.TypeLevel.Num.Ops ( Data/TypeLevel/Num/Ops.hs, interpreted )

Data/TypeLevel/Num/Ops.hs:90:10:
    Illegal instance declaration for ‘Succ' (x, x) (x, x) D0 D0 True’
      The liberal coverage condition fails in class ‘Succ'’
        for functional dependency: ‘yh yl yz -> xh xl’
      Reason: lhs types ‘D0’, ‘D0’, ‘True’
        do not jointly determine rhs types ‘(x, x)’, ‘(x, x)’
    In the instance declaration for ‘Succ' (x, x) (x, x) D0 D0 True’
...

Typechecked fine on ghc-7.6.3

[1 of 8] Compiling Data.TypeLevel.Num.Reps ( Data/TypeLevel/Num/Reps.hs, interpreted )
[2 of 8] Compiling Data.TypeLevel.Num.Sets ( Data/TypeLevel/Num/Sets.hs, interpreted )
[3 of 8] Compiling Data.TypeLevel.Num.Aliases.TH ( Data/TypeLevel/Num/Aliases/TH.hs, interpreted )
[4 of 8] Compiling Data.TypeLevel.Num.Aliases ( Data/TypeLevel/Num/Aliases.hs, interpreted )
Generating and compiling a zillion numerical type aliases, this might take a while
[5 of 8] Compiling Data.TypeLevel.Bool ( Data/TypeLevel/Bool.hs, interpreted )
[6 of 8] Compiling Data.TypeLevel.Num.Ops ( Data/TypeLevel/Num/Ops.hs, interpreted )
[7 of 8] Compiling Data.TypeLevel.Num ( Data/TypeLevel/Num.hs, interpreted )
[8 of 8] Compiling Data.TypeLevel   ( Data/TypeLevel.hs, interpreted )
Ok, modules loaded: Data.TypeLevel, Data.TypeLevel.Num, Data.TypeLevel.Bool, Data.TypeLevel.Num.Reps, Data.TypeLevel.Num.Aliases, Data.TypeLevel.Num.Sets, Data.TypeLevel.Num.Ops, Data.TypeLevel.Num.Aliases.TH.
*Data.TypeLevel>

I have failed to decipher an error message, but looks like it tries to instantiate
a thing it should not.

My apologies if it's not-a-bug.

Attachments (1)

type-level-0.2.4.tar.gz (11.4 KB) - added by slyfox 14 months ago.
type-level-0.2.4.tar.gz

Download all attachments as: .zip

Change History (19)

Changed 14 months ago by slyfox

type-level-0.2.4.tar.gz

comment:1 Changed 14 months ago by rwbarton

  • Resolution set to invalid
  • Status changed from new to closed

The error looks correct to me.

class Succ' xh xl yh yl yz | xh xl -> yh yl yz, yh yl yz -> xh xl
instance Failure (PredecessorOfZeroError x) => Succ' (x,x) (x,x) D0 D0 True

The functional dependency yh yl yz -> xh xl is violated because D0 D0 True do not determine (x,x) (x,x): x is free. An instance of #8634. I'm going to mark this ticket as invalid (since it seems to me that you are considering this as a regression rather than a feature request), but see that ticket and its related tickets for ongoing discussion.

comment:2 Changed 13 months ago by augustss

The documentation says 'Both the Paterson Conditions and the Coverage Condition are lifted if you give the -XUndecidableInstances flag'.

This doesn't seem to be the case. And why does it matter that x is free? Can't it just be assumed to be universally quantified?

It would be nice to get back whatever behaviour the old ghc had, because it did the right thing for this case.

comment:3 Changed 13 months ago by simonpj

Would anyone who knows or cares about functional dependencies like to look into this? I could look at it myself, but I'll do so only if someone says it is mission-critical to them. Thanks!

Simon

Last edited 13 months ago by simonpj (previous) (diff)

comment:4 Changed 13 months ago by simonpj

  • Cc dreixel diatchki added

comment:5 Changed 8 months ago by slyfox

Should the ticket be reopened not to get lost and final decision to be stated?

Thanks!

comment:6 Changed 8 months ago by simonpj

  • Resolution invalid deleted
  • Status changed from closed to new

Yes, I'll re-open it. But lacking someone who cares about functional dependencies, it's a bit in limbo. Fundep enthusiasts, stand forth!

Simon

comment:7 Changed 5 months ago by jstolarek

I've just run into this problem trying to run this toy example from Haskell Wiki:

data Zero
data Succ a

class Add a b ab | a b -> ab, a ab -> b
instance Add Zero b b
instance (Add a b ab) => Add (Succ a) b (Succ ab)
Illegal instance declaration for ‘Add (Succ a) b (Succ ab)’
  The liberal coverage condition fails in class ‘Add’
    for functional dependency: ‘a b -> ab’
  Reason: lhs types ‘Succ a’, ‘b’
    do not jointly determine rhs type ‘Succ ab’
In the instance declaration for ‘Add (Succ a) b (Succ ab)’

Interestingly, replacing empty data declarations of Zero and Succ a with data kinds makes the code compile:

data Nat = Zero | Succ Nat

class Add a b ab | a b -> ab, a ab -> b
instance Add Zero b b
instance (Add a b ab) => Add (Succ a) b (Succ ab)

Why with empty data types this is wrong but with promoted types everything is fine? Also, HEAD complains about redundant constraint:

Redundant constraint: Add a b ab
In the instance declaration for ‘Add ('Succ a) b ('Succ ab)’

comment:8 Changed 5 months ago by goldfire

My guess is that PolyKinds is causing trouble in the not-promoted case. Do you have PolyKinds enabled? Try running with -fprint-explicit-kinds.

But, the "redundant constraint" warning is almost certainly wrong. I would post that as a separate bug, which we should try to fix by 7.10, I think.

comment:9 Changed 5 months ago by jstolarek

My guess is that PolyKinds is causing trouble in the not-promoted case.

Spot-on. Without PolyKinds this works perfectly fine.

But, the "redundant constraint" warning is almost certainly wrong.

Yes. Now that the non-promoted version compiles it produces the same warning. I'll fill a bug report.

comment:10 follow-up: Changed 5 months ago by jstolarek

My guess is that PolyKinds is causing trouble in the not-promoted case.

I have to ask: how did you figure that out? I don;t see anything in the error message (nor in the code) that would suggest PolyKinds are causing the problem.

comment:11 Changed 4 months ago by simonpj

OK, so aside from the "redundant constraint" problem (now reported as #10100), what's left in this ticket?

  • The error message looks absolutely right to me.
    Data/TypeLevel/Num/Ops.hs:90:10:
        Illegal instance declaration for ‘Succ' (x, x) (x, x) D0 D0 True’
          The liberal coverage condition fails in class ‘Succ'’
            for functional dependency: ‘yh yl yz -> xh xl’
          Reason: lhs types ‘D0’, ‘D0’, ‘True’
            do not jointly determine rhs types ‘(x, x)’, ‘(x, x)’
        In the instance declaration for ‘Succ' (x, x) (x, x) D0 D0 True’
    


  • Yes, the user manual about "lifting the Paterson conditions" is wrong: see #8634, comment:14.
  • If, for some reason, this code is really really what you want, then you need DysFunctionalDependencies; for that see #8634.

So can we close this ticket?

Simon

comment:12 Changed 4 months ago by jstolarek

Looking again at my comment:7 I believe it is a bug that enabling PolyKinds breaks a correct program. That's of course not related to the original bug and deserves its separate bug report.

comment:13 follow-up: Changed 4 months ago by simonpj

OK go ahead an open another ticket, and close this one. But as you'll see with -fprint-explicit-kinds, the coverage condition really is violated. You may say it's a bug but I don't see a reasonable way to fix it. (A better error message would be good, I grant you.)

Simon

comment:14 in reply to: ↑ 13 ; follow-up: Changed 4 months ago by jstolarek

  • Resolution set to fixed
  • Status changed from new to closed

Replying to simonpj:

But as you'll see with -fprint-explicit-kinds, the coverage condition really is violated.

I'm looking at the error message with -fprint-explicit-kinds and I don't see how the coverage condition is violated here :-/

Illegal instance declaration for
  ‘Add * k * (Succ k a) b (Succ k ab)’
  The liberal coverage condition fails in class ‘Add’
    for functional dependency: ‘a b -> ab’
  Reason: lhs types ‘Succ k a’, ‘b’
    do not jointly determine rhs type ‘Succ k ab’
In the instance declaration for ‘Add (Succ a) b (Succ ab)’

But if you say this is correct then I trust your judgement. Closing this ticket.

comment:15 Changed 4 months ago by jstolarek

  • Resolution fixed deleted
  • Status changed from closed to new

Wrong resolution, sorry. Reopening.

comment:16 Changed 4 months ago by jstolarek

  • Resolution set to invalid
  • Status changed from new to closed

...and closing as invalid.

comment:17 in reply to: ↑ 10 Changed 4 months ago by goldfire

Replying to jstolarek:

I have to ask: how did you figure that out? I don;t see anything in the error message (nor in the code) that would suggest PolyKinds are causing the problem.

I was just trying to figure out what could possibly be different between the two cases. With PolyKinds on, the empty-datatype method produces an extra degree of freedom, in the kind of the parameter to Succ. Seeing nothing else which could be causing difficulty, I thought PolyKinds would have to be the problem.

comment:18 in reply to: ↑ 14 Changed 4 months ago by goldfire

I agree with Janek that the coverage condition shouldn't fail there. I've opened a new ticket #10109 to explore that part, as this ticket has gotten a little muddled, and the previous discussion isn't helpful (in my opinion) in understanding #10109.

Note: See TracTickets for help on using tickets.