Opened 15 months ago
Closed 14 months ago
#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
Version: | 8.4.3 → 8.5 |
---|
comment:2 Changed 15 months ago by
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 follow-up: 4 Changed 15 months ago by
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 Changed 15 months ago by
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
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:7 Changed 15 months ago by
Cc: | Iceland_jack added |
---|
comment:9 follow-up: 10 Changed 15 months ago by
Status: | new → merge |
---|---|
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 Changed 15 months ago by
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
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
Milestone: | 8.6.1 → 8.8.1 |
---|---|
Resolution: | → fixed |
Status: | merge → closed |
Unfortunately this looks to be a bit large to backport to 8.6.
This is actually for version
8.6.0
but there isn't such an option in the box...