On Wed, Oct 13, 2010 at 12:13:29PM +0400, Eugene Kirpichov wrote:
Hm. This is not actually an answer to your question, just a "discussion starter", but still.
The code below typechecks, though actually it shouldn't: there's no type "n" such that "ones" is formed by the FL from some value of type List Int n. Or should it?
{-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls #-} module Finite where
data Zero data Succ a
class Finite a where
instance Finite Zero instance (Finite a) => Finite (Succ a)
data List a n where Nil :: List a Zero Cons :: (Finite n) => a -> List a n -> List a (Succ n)
data FiniteList a where FL :: (Finite n) => List a n -> FiniteList a
nil :: FiniteList a nil = FL Nil
cons :: a -> FiniteList a -> FiniteList a cons a (FL x) = FL (Cons a x)
list123 = cons 1 (cons 2 (cons 3 nil))
ones = cons 1 ones -- typechecks ok
Fascinating. Doing ones' = Cons 1 ones' of course does not typecheck (as expected) with an occurs check error (can't unify n = S n). But ones = cons 1 ones does typecheck. And it makes sense: I can see why cons has the type it does, and given that type for cons this definition of ones is perfectly well-typed. But the upshot, which I had never considered, seems to be that existentially quantified types are allowed to be _|_. -Brent