Opened 4 years ago

Last modified 3 years ago

## #10338 new bug

# GHC Forgets Constraints

Reported by: | crockeea | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 7.8.3 |

Keywords: | Cc: | ||

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description (last modified by )

This is possibly fixed by #10195, but I don't have a convenient means of testing it. At any rate, this testcase is considerably simpler than the one in #10195.

{-# LANGUAGE TypeFamilies, FlexibleContexts, GADTs, MultiParamTypeClasses #-} type family F r class (Functor t) => T t r where fromScalar :: r -> t r data Foo t r where Foo :: t (F r) -> Foo t r Scalar :: r -> Foo t r toF :: r -> F r toF = undefined convert :: (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = let fromScalar' = fromScalar in Foo $ fromScalar' $ toF c

This code compiles with GHC 7.8.4.

When I add a generic instance for `T`

(which requires `FlexibleInstances`

): `instance (Functor t, Num r) => T t r`

GHC complains:

Could not deduce (Num (F r)) arising from a use of ‘fromScalar’ from the context (T t (F r)) bound by the type signature for convert :: (T t (F r)) => Foo t r -> Foo t r at Main.hs:(17,12)-(18,23) In the expression: fromScalar In an equation for ‘fromScalar'’: fromScalar' = fromScalar In the expression: let fromScalar' = fromScalar in Foo $ fromScalar' $ toF c

Of course the problem can be fixed by adding a type signature to `fromScalar`

and adding `ScopedTypeVariables`

:

convert :: forall t r . (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = let fromScalar' = fromScalar :: F r -> t (F r) in Foo $ fromScalar' $ toF c

Like #10195, this is triggered when a generic instance is in scope. The (main) problem of course is that GHC tries to match the generic instance instead of using the `T t (F r)`

constraint supplied by `convert`

.

A secondary issue is that I think the example should have the same behavior pre- and post-instance, i.e either both should compile or both should not compile. I'm not sure if a monomorphism restriction is actually being triggered here or if that's just a red herring.

### Change History (8)

### comment:1 Changed 4 years ago by

### comment:2 Changed 4 years ago by

The fact that the binding of `fromScalar'`

is a local one is not actually important here: the program with

instance (Functor t, Num r) => T t r fromScalar' a = fromScalar a -- or turn on NoMonomorphismRestriction convert :: (T t (F r)) => Foo t r -> Foo t r convert (Scalar c) = Foo $ fromScalar' $ toF c

also gives the error about "Could not deduce (Num (F r)) arising from a use of ‘fromScalar'’".

### comment:3 Changed 4 years ago by

But that's very reasonable isn't it? What type do you expect to be inferred for `fromScalar'`

? Well, you get a constraint `T t r`

arising from the call to `fromScalar`

in its RHS, and GHC solves that constraint using the instance declaration, so we get the inferred type

fromScalar' :: (Functor t, Num r) => r -> t r

And now you can see why you get the complaint when it's called in `convert`

.

What did you think would happen?

### comment:4 Changed 4 years ago by

Edit: Future readers, please ignore this comment which is just noise.

~~I've got a new test case for what I assume is this bug. Unfortunately, I can't find a workaround in this case.~~

{-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables, ConstraintKinds, KindSignatures, TypeFamilies, FlexibleInstances #-} import GHC.Prim import Control.Monad class Unsat (a :: * -> *) c class Qux (t :: * -> *) where type QCtx t q :: Constraint qux :: (QCtx t q, Monad rnd) => v -> rnd (t q) instance Qux t where type QCtx t q = (Unsat t q) class (Qux c) => C (c :: * -> *) r mymap :: c Double -> c i mymap = undefined foo :: forall c z v rnd . (C c z, Monad rnd, Num z) => v -> rnd (c z) foo svar = liftM mymap $ qux svar

~~I've tried a wide array of explicit type sigs on ~~
`foo`

, but nothing seems to make it find the dictionary for `Qux`

inherited from `C`

.

### comment:5 Changed 4 years ago by

Well all the GHCs I have say

T10338a.hs:27:26: Could not deduce (Unsat c Double) arising from a use of `qux' from the context (C c z, Monad rnd, Num z) bound by the type signature for foo :: (C c z, Monad rnd, Num z) => v -> rnd (c z) at T10338a.hs:26:8-69

And that is totally correct. Every call to `qux`

gives rise to a constraint `QCtx t q`

. Nothing provides that constraint, certainly not `C c z`

. But in fact the instance for `Qux t`

says that `QCtx t q`

simplifies to `Unsat t q`

. And we are stuck.

(The call to `qux`

also gives rise to a `Qux c`

constraint, and that is indeed satisfied from the `C c z`

superclass.)

I'm at a loss for why you think this program should typecheck.

### comment:6 Changed 4 years ago by

Ah, I see. I saw "could not deduce Unsat" and thought it was the same bug. My mistake.

### comment:7 Changed 3 years ago by

If you're not using overlapping instances, then you can solve the problem by imposing

class (Functor t, Num r) => T t r where

In that context, the only (hypothetical) downside is that you don't have the option of hiding the constraint. I don't know if that's a real concern.

If you are using overlapping instances, ~~you've dug yourself into a hole and I don't have much sympathy for you~~ the `ScopedTypeVariables`

work-around doesn't seem too onerous.

It would be interesting to see if this can be reproduced using code that makes sense *without* `OverlappingInstances`

.

### comment:8 Changed 3 years ago by

Description: | modified (diff) |
---|

**Note:**See TracTickets for help on using tickets.

Yes this is confusing. No it's not #10195.

Here's what happens. When GHC comes across the local binding

`let fromScalar' = fromScalar`

, it tries to find its most general type. To do so it instantiates the call to`fromScalar`

with fresh unification variables`t0`

and`r0`

, and generates the constraint`T t0 r0`

. Now it tries to simplify that constraint, and succeeds with the top level instance declaration; and that is where things go wrong; we get the inferred typeWhy doesn't it refrain from simplifying

`T t0 r0`

because of the in-scope constraint`T t (F r)`

? Answer: the most general type of a local binding is computed by calling the constraint simplifer during constraint generation. It's a break with the general plan to first do constraint generation and only then simplify constraints.If we didn't attempt to generalise the binding for

`fromScalar'`

we would not do this early call to the constraint solver, and all would be well (at this point the "given overlap" fix in #10195 would kick in).You might think that

`MonoLocalBinds`

would make this happen, but actually`MonoLocalBinds`

attempts to generalise even local bindings that have no non-top-level type variables, such as this one. And indeed usually generalising is a good thing. Maybe there should be a way to turn off local generalisation altogether.Congratulations on dicovering this. I had previously thought that

`MonoLocalBinds`

would make the constraint solver completely well behaved, but this example shows that I wasn't quite right.I don't see an easy fix, and it seems very much a corner case so probably doesn't justify the work (and code complexity) for a non-easy fix.