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

[Conal Elliott]

>
> > 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 <ryani.spam at gmail.com> 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 <conal at 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
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20081116/f24e6cf3/attachment.htm