#15636 closed bug (fixed)

Implication constraint priority breaks default class implementations

Reported by: i-am-tom Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.6.1-beta1
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Hello,

Not 100% sure that this is a bug, but I've done some investigating (with a lot of help from Csongor Kiss) and thought it was, at the very least, behaviour worth clarifying. The following code...

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where

class D a where
  f :: a -> String
  g :: a -> String
  g = f

class C a

instance (forall a. C a => D a) => D x where
  f _ = "uh oh"

... produces the error:

    • Could not deduce (C x) arising from a use of ‘Test.$dmg’
      from the context: forall a. C a => D a
        bound by the instance declaration at Test.hs:19:10-38
      Possible fix: add (C x) to the context of the instance declaration
    • In the expression: Test.$dmg @(x)
      In an equation for ‘g’: g = Test.$dmg @(x)
      In the instance declaration for ‘D x’
   |
19 | instance (forall a. C a => D a) => D x where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It appears that the problem here is with the default implementation for g. Namely, when f is called, two matching instances are found:

  • forall a. C a => D a
  • (forall a. C a => D a) => D x

The issue, as far as we can tell, is that the first instance is chosen (and then the constraint check fails). I'm currently working around this by introducing a newtype into the head of the quantified constraint†, but I thought it best to check whether this is a bug or, indeed, the expected behaviour in this situation.

Let me know if I've missed anything from this ticket - it's my first one!

Thanks, Tom

† An example of this can be found at https://github.com/i-am-tom/learn-me-a-haskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs#L92-L94

Change History (3)

comment:1 Changed 12 months ago by simonpj

This happens just the same if you say

instance (forall a. C a => D a) => D x where
  f _ = "uh oh"
  g   = f

Why? Well f :: D a => a -> String, so the occurrence of f on the RHS of g's defn here means that we need D x. How can we solve D x?

  • We can solve it from the quantified constraint, giving rise to a need for C x
  • We can solve it from the top level instance instance ... => D x.

GHC picks the first, treating "local" constraints as shadowing "global" ones. The user manual specifies this. There was some discussion in the GHC proposal thread.

So currently it's by-design. If you want to propose a different design, by all means do so!

comment:2 Changed 12 months ago by i-am-tom

Not at all - if this is intended behaviour, I'm happy to close the ticket. Thanks for the explanation!

comment:3 Changed 12 months ago by i-am-tom

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.