[Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)

[Max Bolingbroke]

On 19 October 2010 19:01, Dan Doel <dan.doel at gmail.com> wrote:
> 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