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 |