RE: GADT problems
Hi Simon,
> | op (Foo GadtValue :: Foo) = () :: ()
>
> The thing is that GHC doesn't know the result type of the
> match *at the match point*. Suppose you had written
>
> op (Foo GadtValue :: Foo) = id (() :: ()) or
> op (Foo GadtValue :: Foo) = if blah then () :: () else () or
> op (Foo GadtValue :: Foo) = let x = blah in () :: ()
>
> The signature is too far "inside". We need to know it from
> "outside".
Ah, this is the crucial bit I've been misunderstanding! Instinctively it
feels that when a GADT can't type check I should be annotating the GADT
part - but that's not the case, I should be annotating the expression
containing both the GADT match and its right-hand side. I think the way
the error message is formatted (add a type signature, followed by giving
the local pattern) seems to hint at this. With this insight I've managed
to fix up all the real problems I was experiencing.
My general method for solving these problems was to find an expression
or statement that enclosed both the left and right hand sides, and add
":: Int" to it. I then recompiled and got an error message saying it
couldn't match Int with . I then replaced Int with
and it worked. It seems surprising that the compiler can't
jump through those hoops for me, but I realise my particular cases may
be uncommon or the complexity may be too great. A nice addition to the
error message would be hinting at where the type signature should go, if
it can reasonably be determined.
> | I think this is the underlying problem I'm getting. For things like
> | list-comps and cases I don't seem to be able to find any
> combination
> | of annotations that works, but that is because I'm not
> using top-level
> | annotations.
>
> Perhaps you can give an example that shows your difficulty?
The following is a fake example I was playing with:
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
module Test where
data E x = E x
data Foo a where
Foo :: Gadt a -> Foo a
data Gadt a where
GadtValue :: a -> Gadt (E a)
g :: [()]
g = [() | Foo (GadtValue _) <- undefined] :: [()]
I couldn't figure out how to supply enough annotations to allow the code
to work.
Thanks
Neil
==
Please access the attached hyperlink for an important electronic communications
disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: GADT problems
On Sunday 14 September 2008 20:27:52 Mariusz Przygodzki wrote: > Maybe "they" were waiting so many years because "they" have never > asked users about what users really need and think about it. What? > "It's not that we hate you (unless we do). It's just that we have > nothing to offer you, and you have nothing to offer us." Since that has absolutely nothing do to with the topic of discussion, or indeed anything Gentoo-related, your quoting of it at me can only be considered a personal attack.
RE: GADT problems
> | > | (case undefined of Foo GadtValue -> ()) :: () -- is rigid
> ...
> |
> | But the first compiles fine, so it seems that the scrutinee doesn't
> | have to always be rigid?
>
> Not for me! Either with 6.8.3 or HEAD. What compiler are you using?
HEAD from last Thursday. The code I'm using is slightly different to
your code, and is attached at the end of the message. Is matching Foo
causing its argument to become rigid?
Thanks
Neil
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
module Test where
data E x = E x
data Foo where
Foo :: Gadt a -> Foo
data Gadt a where
GadtValue :: Gadt (E a)
g :: ()
g = case undefined of
Foo GadtValue -> ()
==
Please access the attached hyperlink for an important electronic communications
disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: GADT problems
Ah -- you used an *existential* there! Yes, existentially-bound type variables
are rigid. They stand for themselves, as it were.
That resolves the mystery -- but it existentials admittedly introduce a new
complication
How should this be clarified?
S
| -Original Message-
| From: Mitchell, Neil [mailto:[EMAIL PROTECTED]
| Sent: 15 September 2008 13:56
| To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
| Subject: RE: GADT problems
|
| > | > | (case undefined of Foo GadtValue -> ()) :: () -- is rigid
| > ...
| > |
| > | But the first compiles fine, so it seems that the scrutinee doesn't
| > | have to always be rigid?
| >
| > Not for me! Either with 6.8.3 or HEAD. What compiler are you using?
|
| HEAD from last Thursday. The code I'm using is slightly different to
| your code, and is attached at the end of the message. Is matching Foo
| causing its argument to become rigid?
|
| Thanks
|
| Neil
|
| {-# LANGUAGE GADTs, ScopedTypeVariables #-}
| module Test where
|
| data E x = E x
|
| data Foo where
| Foo :: Gadt a -> Foo
|
| data Gadt a where
| GadtValue :: Gadt (E a)
|
| g :: ()
| g = case undefined of
| Foo GadtValue -> ()
|
| ==
| Please access the attached hyperlink for an important electronic
communications disclaimer:
|
| http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
| ==
|
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: GADT problems
[sent to list as well this time] On Mon, 2008-09-15 at 14:00 +0100, Simon Peyton-Jones wrote: > Ah -- you used an *existential* there! Yes, existentially-bound type > variables are rigid. They stand for themselves, as it were. > > That resolves the mystery -- but it existentials admittedly introduce a new > complication > > How should this be clarified? > For me, "existentially-bound variables are rigid" works well enough. They're a somewhat non-obvious case of 'coming from an annotation' though, and it does warrant mention. -- Philippa Cowderoy <[EMAIL PROTECTED]> ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: GADT problems
> Ah -- you used an *existential* there! Yes, > existentially-bound type variables are rigid. They stand for > themselves, as it were. > How should this be clarified? I'd leave it. I wanted a simple set of rules stating "_if_ you provide the following type signatures your code _will_ compile", which is what you currently provide, albeit I interpreted 'result' slightly differently. If people want to learn where these type signatures can be omitted (because a type is already rigid) people can follow the papers, or learn by trial and error. Thanks Neil == Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html == ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT problems
On Mon, Sep 15, 2008 at 4:18 AM, Simon Peyton-Jones <[EMAIL PROTECTED]> wrote: > > If you can suggest improvements to the manual I'm all ears. Notably, it says > nothing about what "rigid" means or how it propagates. A good solid definition of rigid would be nice. You pointed me at a paper on wobbly types that I found to be quite helpful in my understanding of the type checking issues. The paper told me that roughly speaking rigid means explicit. Once I was armed with just that information I started tackling more and more of these type check problems. Thanks, Jason ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
