Re: "A lazy (~) pattern cannot bind existential type variables"?

...

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"?

I'd expect bottom, just as with matching ~(x,y) against bottom. The lambda is not the same as the "where" clause. Let's desugar a few

of the code snippets you gave me: [...]

Thanks. I get it now, and I see that the only version that makes it through the type-checker is the one that defeats laziness and therefore generally breaks these nice morphism properties. That algebraic failure seems reason enough to try fixing ghc. - Conal On Sun, Nov 16, 2008 at 2:18 AM, Ryan Ingram wrote:

...

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 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