Regarding coherence and implication loops in presence of QuantifiedConstraints

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

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture