[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:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"45f44e2c9d5db2f25c52abb402f197c20579400f/ghc" 45f44e2/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="45f44e2c9d5db2f25c52abb402f197c20579400f"
 Refactor validity checking for constraints

 There are several changes here.

 * TcInteract has gotten too big, so I moved all the class-instance
   matching out of TcInteract into a new module ClsInst. It parallels
   the FamInst module.

   The main export of ClsInst is matchGlobalInst.
   This now works in TcM not TcS.

 * A big reason to make matchGlobalInst work in TcM is that we can
   then use it from TcValidity.checkSimplifiableClassConstraint.
   That extends checkSimplifiableClassConstraint to work uniformly
   for built-in instances, which means that we now get a warning
   if we have givens (Typeable x, KnownNat n); see Trac #15322.

 * This change also made me refactor LookupInstResult, in particular
   by adding the InstanceWhat field.  I also changed the name of the
   type to ClsInstResult.

   Then instead of matchGlobalInst reporting a staging error (which is
   inappropriate for the call from TcValidity), we can do so in
   TcInteract.checkInstanceOK.

 * In TcValidity, we now check quantified constraints for termination.
   For example, this signature should be rejected:
      f :: (forall a. Eq (m a) => Eq (m a)) => blah
   as discussed in Trac #15316.   The main change here is that
   TcValidity.check_pred_help now uses classifyPredType, and has a
   case for ForAllPred which it didn't before.

   This had knock-on refactoring effects in TcValidity.
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15316#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler