Opened 2 years ago

Closed 19 months ago

Last modified 19 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 Rev(s):
Wiki Page:

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 2 years ago.
type-level-0.2.4.tar.gz

Download all attachments as: .zip

Change History (19)

Changed 2 years ago by slyfox

type-level-0.2.4.tar.gz

comment:1 Changed 2 years 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 2 years 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 2 years 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 2 years ago by simonpj (previous) (diff)

comment:4 Changed 2 years ago by simonpj

  • Cc dreixel diatchki added

comment:5 Changed 2 years ago by slyfox

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

Thanks!

comment:6 Changed 23 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 20 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 20 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 20 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 20 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 19 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 19 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 19 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 19 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 19 months ago by jstolarek

  • Resolution fixed deleted
  • Status changed from closed to new

Wrong resolution, sorry. Reopening.

comment:16 Changed 19 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 19 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 19 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.