On 19 October 2010 19:01, Dan Doel
However, this argument is a bit circular, since that eliminator could be defined to behave similarly to an irrefutable match.
Right.
Or, put another way, eta expansion of a dictionary-holding existential would result in a value holding a bottom dictionary, whereas that's otherwise impossible, I think.
I think evaluating dictionaries strictly is more of a "want to have" rather than "actually implemented". In particular, GHC supports building value-recursive dictionaries - and making dictionary arguments strict indiscriminately would make this feature rather useless. I think this means that even with constrained existential things would be OK. What is definitely not OK is lazy pattern matching on GADTs which have *type equality* constraints on their existentials - because the type equalities are erased at compile time, lazy pattern matching on a GADT would leave no opportunity for us to observe that the proof of the type equality was bogus (a bottom) - so allowing this would let our programs segfault. For example, this program would erroneously typecheck: """ data Eq a b where Eq :: EQ a a f :: Eq Int Bool -> Bool f (~Eq) = ((1 :: Int) + 1) :: Bool main = print $ f undefined """ I'm sticking with my unsafeCoerce based solution for now. It's ugly, but it's nicely *localised* ugliness :-) Cheers, Max