The problem is that the representation probably does not reduce to a normal form. Say, for the case type instance F (Nest a) x = Either() (a,F a x) fnn :: F (Nest a) (Nest a) fnn = Left () it compiles ok. But why can't the representation be infinite, like any other infinite data type? Cheers, hugo On Mon, Apr 7, 2008 at 10:30 PM, Hugo Pacheco <hpacheco@gmail.com> wrote:

Hi guys, I have been experimenting some weird stuff (risky, yes I know) but the behaviour was certainly not the one I expected:

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Nest where

data Nest a = Nil | Cons a (Nest (a,a))

type family F a x :: * type instance F (Nest a) x = Either () (a,F (Nest (a,a)) x)

fnn :: F (Nest Int) (Nest Int) fnn = Left ()

The following module fails to compile (or better, compilation never ends).

Maybe there is something very bad going on due to the undecidable-instances extension?

Any clue? hugo

The type system requires strong normalization. By specifying "allow-undecidable-instances", you are agreeing to provide proofs of strong normalization outside of the compiler, instead of relying on the compiler to derive them for you. Because you have claimed that your instance is strongly normalizing, the compiler is attempting to evaluate your type to normal form, in order to verify that fnn has the correct type... F (Nest Int) (Nest Int) ~ Either () (Nest Int, F (Nest (Int, Int)) (Nest Int) ~ Either () (Nest Int, Either () (Nest (Int, Int), F (Nest ((Int,Int),(Int,Int)) (Nest Int))) ~ ... There is no concrete type for the type system to hold on to here; if this was allowed we get _|_ at the type level which I suspect makes the type system inconsistent. You can break the infinite recursion with a newtype, which gives the type system a concrete type to hold on to. This works: {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} module Nest where data Nest a type family F a x :: * newtype FWrap a x = FWrap (F a x) type instance F (Nest a) x = Either () (a, FWrap (Nest (a,a)) x) fnn :: F (Nest Int) (Nest Int) fnn = Left () fnn2 :: F (Nest Int) (Nest Int) fnn2 = Right (1, FWrap (Right ((2,3), FWrap (Left ())))) Some comments: 1) You don't ever use the contents of Nest so I reduced it to an empty datatype; it's just a constructor for F to case against.. 2) You never use the "x" argument of F; is that intentional? -- ryan On 4/7/08, Hugo Pacheco <hpacheco@gmail.com> wrote:

Hi guys,

I have been experimenting some weird stuff (risky, yes I know) but the behaviour was certainly not the one I expected:

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Nest where

data Nest a = Nil | Cons a (Nest (a,a))

type family F a x :: * type instance F (Nest a) x = Either () (a,F (Nest (a,a)) x)

fnn :: F (Nest Int) (Nest Int) fnn = Left ()

The following module fails to compile (or better, compilation never ends).

Maybe there is something very bad going on due to the undecidable-instances extension?

Any clue? hugo _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe