[GHC] #15316: Regarding coherence and implication loops in presence of QuantifiedConstraints

[GHC]

#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