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