[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:                    |
-------------------------------------+-------------------------------------
Description changed by Ptival:

Old description:

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

New description:

 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 fell within the "loops
 that should be caught by the compiler".

--

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