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

22 Feb 2017

      #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
           Keywords:                 |  Operating System:  Unknown/Multiple
  UndecidableInstances loop          |
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I'm afraid this will simply be seen as "that's what happens when you use
 UndecidableInstances", but I might as well document this issue I had.

 Trying to play with a "Trees that Grow" syntax, I encountered an issue
 when making a mistake, that can be boiled down to the following:

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

 module Loop where

 import GHC.Exts        (Constraint)
 import Test.QuickCheck

 type family X_Var ξ

 data TermX ξ = Var (X_Var ξ)

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

 --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

 }}}

 This code will compile correctly, and generate:

 {{{#!hs
 genTerm :: (X_Var ξ ~ TermX ξ, Arbitrary (TermX ξ), Eq t, Num t) => t ->
 Gen (TermX ξ)
 }}}

 Which is correct (though, not the type I had intended, since my code had a
 mistake).

 Now, if you uncomment the "instance" line only, the compiler will loop.

 Adding the commented out type, of course, gives a type error where it's
 due.

 I was just wondering whether this type of error failed with the loops that
 should be caught by the compiler.

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