Opened 4 years ago

Closed 4 years ago

#7558 closed bug (fixed)

Terrible error message when given and wanted are both insoluble

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone: 7.8.1
Component: Compiler Version: 7.6.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: gadt/T7558
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


In fixing the ambiguity check I came across this tricky program

data T a b where
  MkT :: (a~Maybe b) => a -> Maybe b -> T a b

f :: T a a -> Bool
f (MkT x y) = [x,y] `seq` True

We get an error message

    Could not deduce (a ~ Maybe a)
    from the context (a ~ Maybe a)
      bound by a pattern with constructor
                 MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b,
               in an equation for `f'
      at Frozen2.hs:12:4-10
      `a' is a rigid type variable bound by
          the type signature for f :: T a a -> Bool at Frozen2.hs:11:6
    Relevant bindings include
      f :: T a a -> Bool (bound at Frozen2.hs:12:1)
      x :: a (bound at Frozen2.hs:12:8)
      y :: Maybe a (bound at Frozen2.hs:12:10)
    In the expression: y
    In the first argument of `seq', namely `[x, y]'
    In the expression: [x, y] `seq` True

This error message is nonsense! It arises becuase the "insolubles" get both a "given" insoluble (a~T a) and a "wanted" insoluble with the same type.

This can also arise, rather more easily, with the new ambiguity check, via an inaccessible context

foo :: forall a. (a ~ T a) => a -> a 

It's a bit obscure, but it needs fixing.

Change History (3)

comment:1 Changed 4 years ago by igloo

Milestone: 7.8.1
Owner: set to simonpj

comment:2 Changed 4 years ago by monoidal

This seems to be fixed in HEAD; can someone verify and possibly add a test?

comment:3 Changed 4 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: gadt/T7558

Good point. Thanks.


Note: See TracTickets for help on using tickets.