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

Ryan Ingram ryani.spam at gmail.com
Mon Apr 7 20:39:32 EDT 2008

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

More information about the Haskell-Cafe mailing list