Ambiguous type variable: it's a red herring!

module Ret where

data Whoops = Whoops Int Int

foo :: Maybe Int
foo = return (case Whoops 1 2 of
  Whoops a -> a
  _ -> 0)

Note that there is a pattern match error in the case statement, which the compiler correctly reports. However, it first reports the following red herring:

ret.hs:6:7: error:
    • Ambiguous type variable ‘m0’ arising from a use of ‘return’
      prevents the constraint ‘(Monad m0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘m0’ should be.
      These potential instances exist:
        instance Monad IO -- Defined in ‘GHC.Base’
        instance Monad Maybe -- Defined in ‘GHC.Base’
        instance Monad ((->) r) -- Defined in ‘GHC.Base’
        ...plus two others
        (use -fprint-potential-instances to see them all)
    • In the expression:
        return
          (case Whoops 1 2 of {
             Whoops a -> a
             _ -> 0 })
      In an equation for ‘foo’:
          foo
            = return
                (case Whoops 1 2 of {
                   Whoops a -> a
                   _ -> 0 })

One would think that the context foo :: Maybe Int is sufficient for the compiler to realize that return (blah) implies that m0 = Maybe, regardless of the errors involved in the expression (blah).

ghc 7.10.3 does not report this red herring. One can get a similar red-herring type error in ghc 7.10.3 by replacing return (...) with return $ ... in the example above.

The red herring also does *not* appear, in ghc 7.10.3 or in ghc 8.0.1, if you name the broken case expression with a let binding.

module Ret where

data Whoops = Whoops Int Int

foo :: Maybe Int
foo = return boo where
  boo = case Whoops 1 2 of
    Whoops a -> a
    _ -> 0

There seems to be something fishy going on here.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

mentioned in issue #12529 (closed)

I think the code below might be affected by the same issue.

data A
data B

class F a where
  f :: a -> B

instance F A where
  f = undefined

g :: (A, B)
g = (x, f x)
  where
--  x :: A
    x = undefined

With GHC 8.0.1, I get:

test.hs:11:9: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘f’
      prevents the constraint ‘(F a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instance exist:
        instance F A -- Defined at test.hs:7:10
    • In the expression: f x
      In the expression: (x, f x)
      In an equation for ‘g’:
          g = (x, f x)
            where
                x = undefined

The code compiles fine if I uncomment the second to last line. However, it seems like GHC should be able to tell that x has type A. I haven't tested other versions of GHC.

The case in ticket:12124#comment:125344 is behaving correctly. The type of x is generalised to x :: forall a. a. So the info from two uses of x in (x, f x) do not communicate with each other.

Even -XMonoLocalBinds does not solve this, because with this flag GHC still generalises local bindings that have no free variables.

I still need to look at the Description; but ticket:12124#comment:125344 looks fine to me.

For the Description, what is happening is this:

• The ill-arity'd pattern Whoops a -> .. makes the typechecker emit an error message and fail with a hard error; rightly so.
• Usually the typing constraints arising from the failing computation would be discarded. But as a short-cut for a common case, GHC does not begin a new implication constraint for the RHS of foo, because it has no tyvars and no given constraints.
• So the Monad a constraint arising from the call of return is accumulated into the top-level constraints of the whole program; so after recovering from the error GHC tries to solve the constraint.

Two possible solutions

• Remove the special case. That looks OK, but it'd mean that we might solve (Num Int) repeatedly in different function definitions. CSE can common-up later, but it's just more work.
• In the special case, accumulate constraints in a separate variable, and union them into the outer context only if the typecheck succeeds. Not hard to do; I think this is probably best.

Thanks for the accurate report!

Simon

mentioned in commit 465c6c5d

All fixed. I'm not sure if it's worth pushing to 8.0.2, but I think it'd be safe to do so.

Simon

Trac metadata

Trac field	Value
Test case	- → typecheck/should_fail/T12124

added 1 deleted label

closed

changed milestone to %8.0.2

Merged to ghc-8.0 as 5662ceae.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

mentioned in commit 2fdf21bf

added Pnormal label

very very very stupid language