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

26 Jun 2018

      #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       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 First of all this piece of code:
 {{{#!hs
 {-# 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:
 {{{#!hs
 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:
 {{{#!hs
 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:
 {{{#!hs
 {-# 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
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15316
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler