[Haskell-cafe] Type Families: infinite compile process?

[Ryan Ingram]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>