[Haskell] simulating dependent types; ghc/ghci discrepancy

John D. Barnett barnett at MIT.EDU
Wed Apr 14 11:13:51 EDT 2004


Hello all-

I'm still playing with simulating dependent types using rank-2 
polymorphism, and I've run into a small stumbling block on unwrapping 
existential datatypes: they can't be let-bound (monomorphic 
restriction?), but can be unwrapped in a case or lambda. Actually, I 
find that assignment in do-notation works nicely (since I'm already 
writing monadic code). As an example:

module DepTest where

data Show' = forall a . Show a => Show' a

print' :: Show' -> IO ()
print' x = do (Show' x') <- return x
	      print x'  -- here, the type of x' is known

test :: IO ()
test = print' (Show' True)


This works fine. My problem is that I'd like to do this interactively, 
in ghci.

*DepTest> :t Show' True
Show' True :: Show'
*DepTest> Show' x <- return $ Show' True
*DepTest> :t x
x :: forall a. a
*DepTest> x
getTcTyVar a {- tv aXJ -}
getTcTyVar a {- tv aXJ -}
getTcTyVar a {- tv aXJ -}
getTcTyVar a {- tv aXJ -}
getTcTyVar a {- tv aXJ -}
getTcTyVar a {- tv aXJ -}
Interrupted.

First, the type of x seems like it should be either Bool or (forall a. 
Show a => a), but not (forall a.a). Second, egads, what did I do?

Is it possible to unwrap an existential type in ghci?

Thanks-

John



More information about the Haskell mailing list