[GHC] #13320: Unfortunate compiler loop when creating type loop (with UndecidableInstances)

[GHC]

#13320: Unfortunate compiler loop when creating type loop (with
UndecidableInstances)
-------------------------------------+-------------------------------------
        Reporter:  Ptival            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
                                     |  UndecidableInstances loop
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Here's a version with no dependencies:

 {{{#!hs
 {-# language ConstraintKinds, FlexibleContexts, TypeFamilies,
 UndecidableInstances #-}

 module Loop where

 import GHC.Exts        (Constraint)

 data QCGen

 newtype Gen a = MkGen { unGen :: QCGen -> Int -> a }

 sized :: (Int -> Gen a) -> Gen a
 sized f = MkGen (\r n -> let MkGen m = f n in m r n)

 class Arbitrary a where
   arbitrary :: Gen a

 type family X_Var ξ

 data TermX ξ = Var (X_Var ξ)

 type ForallX (φ :: * -> Constraint) ξ = ( φ (X_Var ξ) )

 -- Uncommenting the line below gives a proper type error.
 --genTerm :: ForallX Arbitrary ξ => Int -> Gen (TermX ξ)
 genTerm 0 = Var <$> arbitrary
 genTerm n = Var <$> genTerm (n - 1)

 instance ForallX Arbitrary ξ => Arbitrary (TermX ξ) where
   arbitrary = sized genTerm
 }}}

 At the very least, compiling this on GHC HEAD doesn't loop forever, but
 instead fails with a stack overflow:

 {{{
 Bug.hs:25:1: error:
     Reduction stack overflow; size = 201
     When simplifying the following type: Arbitrary (TermX ξ0)
     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)
    |
 25 | genTerm 0 = Var <$> arbitrary
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
 }}}

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