[GHC] #15888: Quantified constraints can be loopy

11 Nov 2018

      #15888: Quantified constraints can be loopy
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.3
          Component:  Compiler       |           Version:  8.6.2
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider this abuse:

 {{{#!hs
 {-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}

 module Bug where

 data T1 a
 data T2 a

 class C a where
   meth :: a

 instance (forall a. C (T2 a)) => C (T1 b) where
   meth = error "instance T1"

 instance (forall a. C (T1 a)) => C (T2 b) where
   meth = error "instance T2"

 example :: T1 Int
 example = meth
 }}}

 GHC says

 {{{
     • Reduction stack overflow; size = 201
       When simplifying the following type: C (T1 a)
       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 expression: meth
       In an equation for ‘example’: example = meth
 }}}

 Of course, I've taken on some responsibility for my actions here by saying
 `UndecidableInstances`, but GHC really should be able to figure this out.
 Here's what's happening:

 1. We get a Wanted `C (T1 Int)`.

 2. GHC chooses the appropriate instance, emitting a Wanted `forall a. C
 (T2 a)`.

 3. GHC skolemizes the `a` to `a1` and tries solve a Wanted `C (T2 a1)`.

 4. GHC chooses the appropriate instance, emitting a Wanted `forall a. C
 (T1 a)`.

 5. GHC skolemizes the `a` to `a2` and tries to solve a Wanted `C (T1 a2)`.

 And around and around we go.

 (This loop is guessed at from knowing GHC's algorithms in general. I did
 not look at a trace.)

 We ''could'' get this one, though. Before skolemizing, we could stash the
 Wanted in the `inert_solved_dicts`, which is where we record uses of top-
 level instances. (See `Note [Solved dictionaries]` in TcSMonad.) Then,
 later, when we see the same Wanted arise again, we would just use the
 cached value, making a well-formed recursive dictionary.

 This deficiency was discovered in `singletons`
 (https://github.com/goldfirere/singletons/issues/371). Perhaps that's not
 "the wild", but it's not quite contrived either.

 Note that we don't need two datatypes to trigger this, but having one
 recursive instance like this seems awfully silly.

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