#15316 closed bug (fixed)

Regarding coherence and implication loops in presence of QuantifiedConstraints

Reported by: mniip Owned by:
Priority: high Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints Cc: simonpj, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: quantified-constraints/T15316
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

First of all this piece of code:

{-# LANGUAGE RankNTypes, QuantifiedConstraints #-}
-- NB: disabling these if enabled:
{-# LANGUAGE NoUndecidableInstances, NoUndecidableSuperClasses #-}

import Data.Proxy

class Class a where
         method :: a

subsume :: (Class a => Class b) => Proxy a -> Proxy b -> ((Class a => Class b) => r) -> r
subsume _ _ x = x

value :: Proxy a -> a
value p = subsume p p method

This produces a nonterminating value even though nothing warranting recursion was used.

Adding:

value' :: Class a => Proxy a -> a
value' p = subsume p p method

Produces a value' that is legitimately equivalent to method in that it equals to the value in the dictionary whenever an instance exists (and doesn't typecheck otherwise). Thus two identical expressions in different instance contexts end up having different values (violating coherence?)

If we add:

joinSubsume :: Proxy a -> ((Class a => Class a) => r) -> r
joinSubsume p x = subsume p p x

The fact that this typechecks suggests that GHC is able to infer Class a => Class a at will, which doesn't seem wrong. However, the fact that Class a is solved from Class a => Class a via an infinite loop of implication constraints is questionable. Probably even outright wrong in absence of UndecidableInstances.

Another issue is the following:

{-# LANGUAGE ConstraintKinds #-}
subsume' :: Proxy c -> ((c => c) => r) -> r
subsume' _ x = x
    • Reduction stack overflow; size = 201
      When simplifying the following type: c
      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the type signature:
        subsume' :: Proxy c -> ((c => c) => r) -> r

Change History (12)

comment:1 Changed 15 months ago by mniip

Version: 8.4.38.5

This is actually for version 8.6.0 but there isn't such an option in the box...

comment:2 Changed 15 months ago by mniip

Cc: simonpj added

After reading the paper ( https://i.cs.hku.hk/~bruno/papers/hs2017.pdf ) I've been able to construct a corecursive proof that "P,_L (C => C) ; Gamma |= C". Such nontermination is somewhat addressed in the section 6 of the paper where Paterson conditions are modified to account for the new features, and indeed, if I say:

data D a = D
instance (forall a. Show a => Show a) => Show (D a)

It complains:

error:
 * The constraint `Show a' is no smaller than the instance head `Show a'
   (Use UndecidableInstances to permit this)
 * In the quantified constraint `forall a. Show a => Show a'
   In the instance declaration for `Show (D x)'

However all of these checks seem to be absent when a higher rank type introduces a local axiom, like in the code in the bug report. The paper also totally ignores higher rank types...

This leads to a question: should forall c. c => c be an inferrable local axiom schema in absence of UndecidableInstances?

If yes, then the termination guarantees in the paper don't hold because they assume no axiom violates the Paterson conditions. There's also no clear way to "fix" the termination guarantees -- this is basically equivalent to proving arbitrary theorems in first order logic. Also is there a good way to allow corecursion for (forall a. Show a => Show (f a)) => Show (Fix f) but not (C => C) => C? Could we corecurse only on the axioms that satisfy paterson conditions?

If no, then ekmett's data a :- b = Sub (a => Dict b) is a category while Dict (a => b) is not. There's also the problem with this type of class that you can find in a few places:

class A a => B a
instance A a => B a

This gives us two axiom schemas: forall a. A a => B a (instance) and forall a. B a => A a (superclass). Composing the two we can derive A a => A a again. So we can't compose arbitrary implications either...

comment:3 Changed 15 months ago by simonpj

This leads to a question: should forall c. c => c be an inferrable local axiom schema in absence of UndecidableInstances?

I think not. I'm busy adding a check for this case! Agreed?

comment:4 in reply to:  3 Changed 15 months ago by mniip

Replying to simonpj:

This leads to a question: should forall c. c => c be an inferrable local axiom schema in absence of UndecidableInstances?

I think not. I'm busy adding a check for this case! Agreed?

What kind of check? Just for the c => c case? Are you sure there aren't any roundabout ways to achieve similar fix id-type corecursion?

comment:5 Changed 15 months ago by simonpj

I meant:

  • Apply the instance-termination check to every quantified constraint (cxt => constraint) appearing anywhere in a type.

So f :: (Show a => Show a) => blah would be rejected just as

instance Show a => Show a

is rejected

comment:6 Changed 15 months ago by mniip

That sounds "sound" to me but not necesasrily "good".

comment:7 Changed 15 months ago by Iceland_jack

Cc: Iceland_jack added

comment:8 Changed 15 months ago by Simon Peyton Jones <simonpj@…>

In 45f44e2/ghc:

Refactor validity checking for constraints

There are several changes here.

* TcInteract has gotten too big, so I moved all the class-instance
  matching out of TcInteract into a new module ClsInst. It parallels
  the FamInst module.

  The main export of ClsInst is matchGlobalInst.
  This now works in TcM not TcS.

* A big reason to make matchGlobalInst work in TcM is that we can
  then use it from TcValidity.checkSimplifiableClassConstraint.
  That extends checkSimplifiableClassConstraint to work uniformly
  for built-in instances, which means that we now get a warning
  if we have givens (Typeable x, KnownNat n); see Trac #15322.

* This change also made me refactor LookupInstResult, in particular
  by adding the InstanceWhat field.  I also changed the name of the
  type to ClsInstResult.

  Then instead of matchGlobalInst reporting a staging error (which is
  inappropriate for the call from TcValidity), we can do so in
  TcInteract.checkInstanceOK.

* In TcValidity, we now check quantified constraints for termination.
  For example, this signature should be rejected:
     f :: (forall a. Eq (m a) => Eq (m a)) => blah
  as discussed in Trac #15316.   The main change here is that
  TcValidity.check_pred_help now uses classifyPredType, and has a
  case for ForAllPred which it didn't before.

  This had knock-on refactoring effects in TcValidity.

comment:9 Changed 15 months ago by simonpj

Status: newmerge
Test Case: quantified-constraints/T15316

OK, so now you need UndecidableInstances to have bad quantified constraints, just as the original proposal said.

Probably worth merging, not crucial

comment:10 in reply to:  9 Changed 15 months ago by mniip

Replying to simonpj:

OK, so now you need UndecidableInstances to have bad quantified constraints, just as the original proposal said.

Doesn't UndecidableInstances imply the typechecking might not terminate, as opposed to a finite typechecking process resulting in a program nonterminating due to poor case of context elaboration?

comment:11 Changed 15 months ago by simonpj

Doesn't UndecidableInstances imply the typechecking might not terminate, as opposed to a finite typechecking process resulting in a program nonterminating due to poor case of context elaboration?

Usually yes, but in the cases above it can mean the latter too.

comment:12 Changed 14 months ago by bgamari

Milestone: 8.6.18.8.1
Resolution: fixed
Status: mergeclosed

Unfortunately this looks to be a bit large to backport to 8.6.

Note: See TracTickets for help on using tickets.