Opened 6 years ago

Closed 4 years ago

#3018 closed bug (fixed)

Constraints of function in record appears to nullifiy instance constraints.

Reported by: ben.kavanagh Owned by: simonpj
Priority: normal Milestone:
Component: Compiler Version: 6.10.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T3018
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

If an field of a record that has constraints in its type, defining a value for this field appears to cause the compiler to ignore outer level constraints declared for an instance.

This problem restricts generic functions written in syb-with-class and replib style to functions that do not have constraints.

Attachments (2)

A.hs (797 bytes) - added by ben.kavanagh 6 years ago.
This is the code that fails.
B.hs (745 bytes) - added by ben.kavanagh 6 years ago.
This is the same program with (Monad m) constraint removed. It compiles.

Download all attachments as: .zip

Change History (5)

Changed 6 years ago by ben.kavanagh

This is the code that fails.

Changed 6 years ago by ben.kavanagh

This is the same program with (Monad m) constraint removed. It compiles.

comment:1 Changed 6 years ago by simonpj

  • difficulty set to Unknown
  • Milestone set to _|_
  • Owner set to simonpj

Here are the key lines of code:

class Subst a t t' where
    subst :: (Monad m) => a -> t -> t' -> m t'

data SubstD a t t' 
  = SubstD (forall m. Monad m => a -> t -> t' -> m t')

instance Data (SubstD a t) t' => Subst a t t'          -- (1)

instance Subst a t t' => Sat (SubstD a t t') where     -- (2)
    dict = SubstD subst

The call to 'subst' on the last line gives rise to a constraint (Subst a t t'). But that constraint can be satisfied in two different ways:

  1. Using the instance declaration for Subst (which matches anything!)
  2. Using the context of the Sat (SubstD ..) instance declaration itself

If GHC uses (1) it gets into a corner it can't get out of, because now it needs (Data (SubstD a t) t'), and that it can't get. The error message is a bit misleading:

T3018.hs:29:28:
    Could not deduce (Data (SubstD a t) t') from the context (Monad m)
      arising from a use of `subst' at T3018.hs:29:28-32

it should really say

 ...from the context (Subst a t t', Monad m)

but that's a bit of a separate matter.

Now, you are hoping that (2) will happen, but I hope you can see that it's delicate. Adding the (Monad m) context just tips things over the edge so that GHC doesn't "see" the (Subst a t t') in the context until too late. But the real problem is that you are asking too much. Here is a simpler example:

f :: Eq [a] => a -> blah
f x = let g :: Int -> Int
          g = ....([x]==[x])...
      in ...

The use of == requires Eq [a], but GHC will probably use the list equality instance to simplify this to Eq a; and then it can't deduce Eq a from Eq [a]. Local constraints that shadow or override global instance declarations are extremely delicate.

All this is perhaps soluble if GHC were to be lazier about solving constraints, and only makes the attempt when it has all the evidence in hand. I'm thinking quite a bit about constraint solving at the moment and will bear that in mind. But I can't offer you an immediate solution. At least I hope I've explained the problem.

comment:2 Changed 4 years ago by simonpj

  • Test Case set to typecheck/should_compile/T3018
  • Type of failure set to None/Unknown

Happily this is now fixed.

comment:3 Changed 4 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
Note: See TracTickets for help on using tickets.