#15231 closed bug (fixed)

UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: quantified-constraints/T15231
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4819
Wiki Page:

Description

Consider this program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Bug where

import Data.Kind

data ECC :: Constraint -> Type -> Type

class Y a
class Z a

instance  c         => Y (ECC c a)
instance (c => Z a) => Z (ECC c a)

I would expect both of these instances to work. But while GHC accepts the Y instance, it rejects the Z instance:

$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:15:10: error:
    • Variable ‘c’ occurs more often
        in the constraint ‘c’ than in the instance head
      (Use UndecidableInstances to permit this)
    • In the instance declaration for ‘Z (ECC c a)’
   |
15 | instance (c => Z a) => Z (ECC c a)
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^

That error message seems completely bogus to me, since c appears once in both the context and instance head in both instances.

Change History (6)

comment:1 Changed 16 months ago by simonpj

GHC is following the proposal (Section 3.7). Specifically, in the quantified predicate c => Z a, c does occur more often in the constraint to the left of the arrow, namely c, than in the head of the quantified constraint Z a.

The error message is poor. How about this?

    • Variable ‘c’ occurs more often
        in the constraint ‘c’ 
        than in the instance head `Z a'
      (Use UndecidableInstances to permit this)
    • In the quantified constraint `c => Z a`
    • In the instance declaration for ‘Z (ECC c a)’

comment:2 Changed 16 months ago by RyanGlScott

Ah, gotcha! That error message does sound like an improvement, yes.

comment:3 Changed 16 months ago by sighingnow

Differential Rev(s): Phab:D4819
Status: newpatch

comment:4 Changed 15 months ago by Ben Gamari <ben@…>

In 91822e4e/ghc:

Add "quantified constraint" context in error message, fix #15231.

This patch adds "quantified constraint" context in error message when
UndecidableInstances checking fails for quantified constraints.
See Trac #15231:comment#1.

This patch also pretty-prints the instance head for better error messages.

Test Plan: make test TEST="T15231"

Reviewers: bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie, carter

GHC Trac Issues: #15231

Differential Revision: https://phabricator.haskell.org/D4819

comment:5 Changed 15 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed in GHC 8.6.

comment:6 Changed 15 months ago by RyanGlScott

Milestone: 8.8.18.6.1
Resolution: fixed
Status: patchclosed
Test Case: quantified-constraints/T15231

Actually, this is in GHC 8.6, so this is fixed.

Note: See TracTickets for help on using tickets.