>     My brain just exploded.

Best compiler error message ever.

I think that existential quantification with lazy matches can do some
crazy things to the type system.

> lazyPair ~(a,b) = (a,b).

So, lazyPair undefined = (undefined, undefined); it makes any pair
"more defined".  But what does this do when you have an existential
context?

> data HasShow = forall a. Show a => HasShow a
> weird ~(HasShow x) = HasShow x

Now, what Show context is referred to by the result of "weird undefined"?

> useShow (HasShow x) = show x
> broken = useShow (weird undefined)

It's likely that there is a way to solve this; you need to force the
pattern match to take place anywhere that the existential type gets
applied (in the System F sense).  But I think that doing so is a lot
more difficult for the compiler author, and it's an edge case in the
language.

The lambda is not the same as the "where" clause.  Let's desugar a few
of the code snippets you gave me:

>       fmap g ~(WC f k) = WC f (fmap g k)

=>   fmap = \g wc -> let (WC f k) = wc in WC f (fmap g k)

>       fmap g wc = WC f (fmap g k)
>         where WC f k = wc

=>   fmap = \g wc -> let (WC f k) = wc in WC f (fmap g k)
(same as above)

>       fmap g = \ (WC f k) -> WC f (fmap g k)

=>  fmap = \g wc -> case wc of (WC f k) -> WC f (fmap g k)
(i.e. the same as not using a lazy pattern at all)

I'll think about this and see if I can come up with a workaround.  I'm
not sure it's possible in GHC.

 -- ryan

On Sat, Nov 15, 2008 at 10:33 PM, Conal Elliott <conal@conal.net> wrote:
> What is the reasoning behind the ghc restriction that "A lazy (~) pattern
> cannot bind existential type variables"?
>
> This error came up for me in the following code:
>
>     -- | Add a continuation.
>     data WithCont h b c = forall a. WC (h b a) (a -> c)
>
>     instance Functor (WithCont h b) where
>       fmap g ~(WC f k) = WC f (fmap g k)
>
> The error message:
>
>     A lazy (~) pattern cannot bind existential type variables
>       `a' is a rigid type variable bound by
>           the constructor `WC' at Data/Zip/FoldL.hs:66:11
>     In the pattern: ~(WC f k)
>
> I also tried this variation:
>
>     instance Functor (WithCont h b) where
>       fmap g wc = WC f (fmap g k)
>         where WC f k = wc
>
> and got this message:
>
>     My brain just exploded.
>     I can't handle pattern bindings for existentially-quantified
> constructors.
>     Instead, use a case-expression, or do-notation, to unpack the
> constructor.
>     In the binding group for
>         WC f k
>     In a pattern binding: WC f k = wc
>
> I can work around these limitations by using a lambda:
>
>     instance Functor (WithCont h b) where
>       fmap g = \ (WC f k) -> WC f (fmap g k)
>
> which I believe is equivalent.  Please correct me if I'm wrong here.
>
> For infix definitions like (<*>), however, this work-around is less
> pleasant.
> For instance,
>
>     (<*>) = \ (WC hf hk) (WC xf xk) ->
>       WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a'))
>
> instead of the prettier but forbidden
>
>     ~(WC hf hk) <*> ~(WC xf xk) =
>       WC (hf `zip` xf) (\ (a,a') -> (hk a) (xk a'))
>
>
> If you're curious what these definitions are about, see
> http://conal.net/blog/posts/enhancing-a-zip/ .
>
> Thanks,   - Conal
>
>