Attached file `implies.hs`

($690).

Attached file `demo.hs`

($644).

test case

Attached file `Bar.hs`

($507).

Attached file `Foo.hs`

($506).

Attached file `4195.patch`

(download).

Attached file `4188-tests.patch`

(download).

fix

Attached file `4188.patch`

(download).

compiler

I might be missing something important, but it seems to me that the answer is very obviously 4. I'm not familiar with the precise language of the standard, but I always understood the rule to be very simple: "thou shalt have no more than one instance of a class for a type in thy program". We're blatantly violating this rule, the question is why GHC is not catching us. I think the answer is that you've come up with a way to distinguish GHC's lazy checking of instance overlap from other compilers' eager checking, to GHC's detriment. There's no use of a `Show One`

instance in `D`

, so GHC doesn't bother to investigate it. If overlap were checked eagerly at imports instead of lazily at use sites, the error would be caught.

Obviously there must be a reason why GHC does lazy rather than eager checking (and I think it might have something to do with `Overlapping`

- and `IncoherentInstances`

?), but I don't know the specifics. What would break if overlap checking were eager?

We could prohibit importing two modules that export conflicting instances. But, that would cause interoperability problems between different modules/packages that define overlapping instances.

Do you mean overlapping instances using `OverlappingInstances`

, or without it? In the latter case I think it's the absence of interoperability problems that should count as a bug.

Fabulous! Köszönöm!

Deplorable syntax bikeshedding:

Perhaps, instead of `pattern`

, `data alias`

? I feel that would be more accurate and descriptive for many cases (when the synonym can also be used on the RHS), though possibly less so for others (pattern-only synonyms). It might also avoid having to reserve a keyword. (As with `TypeFamilies`

, as far as I can tell, "family" is not a keyword. I don't think it's possible to avoid the keyword with a new top-level entity like `pattern`

, but maybe I'm mistaken?)

I know about it (referenced it actually in an earlier comment), thanks! I don't think I have an actual practical problem to be worked around. I was just experimenting, exploring, and testing the limits of what's possible. As usual I hit them.

Might the reason for the separation have been that type inference is in theory decidable for rank-2 types, but not higher? I'm not a type theorist but I found this for example: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.1202 (WRT the deprecation/aliasing proposal itself I don't have an opinion)

If instead of Proxy (Foo f) I write Proxy (Bar f) or Proxy f, there is no error.

Triggered by the following code:

```
{-# LANGUAGE PolyKinds, GADTs #-}
data Proxy a
class Foo a where
foo :: a ~ f i => Proxy (Foo f)
```

GHC writes:

```
test.hs:6:34:
Expecting one more argument to `f'
In the type `a ~ f i => Proxy (Foo f)'
In the class declaration for `Foo'
```

It seems to me that given Foo :: forall k. k -> Constraint, Proxy :: forall k. k -> *, a :: k, f :: k1 -> k, that Foo in Proxy (Foo f) should be instantiated at k1 -> k, and Proxy at Constraint, and that this should work.

Trac field | Value |
---|---|

Version | 7.6.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

Newtype deriving doesn't currently work on classes with ATs:

```
test231.hs:19:35:
Can't make a derived instance of `Marshal (Age a)'
(even with cunning newtype deriving):
the class has associated types
In the newtype declaration for `Age'
```

Just to amuse matters further, these both work, with both 7.0 and 7.4:

```
foo :: (Num a, b ~ T a) => a -> b
{-# SPECIALISE foo :: b ~ Bool => Int -> b #-}
```

```
foo :: (Num a, b ~ T a) => a -> b
{-# SPECIALISE foo :: Int -> Bool #-}
```

that is, completely the opposite of the original example, now it works if and only if I *do* expand the type family, and it doesn't matter what I do with the equality constraint.

(FTR I'm testing with 7.0 and 7.4 because I don't have a 7.2 on hand.)

With GHC 7.0 the message was at least a bit less noisy:

```
RULE left-hand side too complicated to desugar
(foo @ Int $dNum)
`cast` (Int -> co :: (Int -> T Int) ~ (Int -> Bool))
```

Also, I can work around it by writing

`{-# SPECIALIZE foo :: Int -> T Int #-}`

that is, leave the type family unexpanded, and then it works.

But if I change the type signature of foo a bit, to introduce a name for T a:

```
foo :: (Num a, b ~ T a) => a -> b
{-# SPECIALIZE foo :: Int -> T Int #-}
```

that breaks again, with the 7.0 error message staying much the same (only an `@ Bool`

and an `@ co`

added to the second line), and the 7.4 message getting considerably uglier:

```
RULE left-hand side too complicated to desugar
case cobox of _ { GHC.Types.Eq# cobox ->
(foo
@ Int
@ Bool
$dNum
(case cobox of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq# @ * @ Bool @ (T Int) @~ cobox
}))
`cast` (<Int> -> cobox :: (Int -> Bool) ~# (Int -> T Int))
}
```

If I once again change the pragma to match the new "shape" of the signature:

`{-# SPECIALISE foo :: b ~ T Int => Int -> b #-}`

then with 7.0 it compiles fine!, while 7.4 outputs this perfect monstrosity:

```
RULE left-hand side too complicated to desugar
let {
cobox :: T Int ~ b
[LclId]
cobox =
case cobox of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq# @ * @ (T Int) @ b @~ (Sym cobox)
} } in
let {
cobox :: b ~ Bool
[LclId]
cobox =
case cobox of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq#
@ * @ b @ Asdf.R:TInt @~ (Sym cobox ; Asdf.TFCo:R:TInt)
} } in
foo
@ Int
@ b
GHC.Num.$fNumInt
(case case case case cobox of _ { GHC.Types.Eq# cobox ->
case cobox of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq# @ * @ (T Int) @ Bool @~ (cobox ; cobox)
}
}
of _ { GHC.Types.Eq# cobox ->
case case cobox of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq# @ * @ Bool @ b @~ (Sym cobox)
}
of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq# @ * @ (T Int) @ b @~ (cobox ; cobox)
}
}
of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq# @ * @ b @ (T Int) @~ (Sym cobox)
}
of _ { GHC.Types.Eq# cobox ->
GHC.Types.Eq# @ * @ b @ (T Int) @~ cobox
})
```

I know this bug is only about the error message, but it seems like that last example might be an actual regression. Should I open a new ticket for it, or is it that "thou shalt not use RULES with type families and expect it to work"?

Right; obviously it's up to you and the rest of the GHC team to figure out what it makes sense to spend time on. This is just to keep track of one of the things that would be nice. Thanks for your time!

The canonical example of what #2893 (closed) lets you write is something like:

`instance (Monad m, forall a. Monoid (m a)) => MonadPlus m where ...`

The example from the paper is:

`instance (Binary a, forall b. Binary b => Binary (f b)) => Binary (GRose f a) where ...`

And the example here was:

`instance (forall a. c a => Show a) => Show (Exists c) where ...`

The way I have it in my head it's not clear to me that #2893 (closed) would, on its own, let you write the latter two examples. To put it simplistically it would you write the `forall`

, but not the `=>`

.

The way I'm reading the second example above is, "if (Binary a), and also (Binary (f b)) follows from (Binary b) for any b, then Binary (GRose f a)". The first example is saying, "if (Monad m), and also (Monoid (m a)) for any a, then (!MonadPlus m)". The difference is that in the !MonadPlus example and all existing Haskell there's noplace where you say "if b follows from a, then c", you only say "if b, then c". But the latter two examples do also have this "if b follows from a, then c" construct. And I think #2893 (closed) is what would let you say the "for any a" part of it, while the feature described by this ticket is what would let you say the "if b follows from a, then" part.

If we look at three simple examples:

`instance forall a. C (A a) => D A where ...`

`instance (C a => C (A a)) => E (A a) where ...`

`instance (forall a. C a => C (A a)) => D A where ...`

then #2893 (closed) (let's call it !QuantifiedConstraints) would let you write the first example, this ticket (let's call it !ImplicationConstraints) would let you write the second example, but only their combination would let you write the third example.

I'm imagining that, with !ImplicationConstraints, (=>) would be a type level operator similar to (~):

```
(~) :: forall k. k -> k -> Constraint
(=>) :: Constraint -> Constraint -> Constraint
```

and you would need !QuantifiedConstraints to be able to use (=>) to also talk about `k1...kN -> Constraint`

s.

I hope this is clearer. Don't hesitate to holler at me if I'm talking nonsense.