#15316: Regarding coherence and implication loops in presence of QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mniip): * cc: simonpj (added) Comment: 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: {{{#!hs 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: {{{#!hs 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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15316#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler