Unfortunate compiler loop when creating type loop (with UndecidableInstances)
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:
{-# 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:
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".