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 crockeea)

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 simonpj

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 type

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

Why 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.

comment:2 Changed 4 years ago by rwbarton

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 simonpj

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 crockeea

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.

Last edited 3 years ago by crockeea (previous) (diff)

comment:5 Changed 4 years ago by simonpj

Well all the GHCs I have say

    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 crockeea

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 dfeuer

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 crockeea

Description: modified (diff)
Note: See TracTickets for help on using tickets.