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