Hi The following code works in GHC 6.8.3, works in GHC 6.9.20071111, but doesn't work in GHC HEAD. {-# 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) f (Foo GadtValue) = True f _ = False Under GHC HEAD I get the error: GADT pattern match with non-rigid result type `t' Solution: add a type signature In the definition of `f': f (Foo GadtValue) = True Adding a type signature to f fixes this problem: f :: Foo -> Bool But I haven't found anywhere other than the top level f to add a type signature. When the match is in a list comprehension, it becomes much harder. While playing further I discovered this example: foos = undefined g = [() | Foo GadtValue <- foos] This code doesn't compile under GHC HEAD, but does under 6.8.3. However, adding the type signature: g :: [()] Makes the code compile. This is surprising, as [()] isn't a GADT type, so shouldn't need stating explicitly. Any help on what these errors mean, or how they can be fixed with local type annotations? Thanks Neil ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
Neil It's by design, and for (I think) good reason. GHC now enforces the rule that in a GADT pattern match - the type of the scrutinee must be rigid - the result type must be rigid - the type of any variable free in the case branch must be rigid Here "rigid" means "fully known to the compiler, usually by way of a type signature". This rule is to make type inference simple and predictable -- it dramatically simplifies inference. To see the issue, ask yourself what is the type of this function data E a where EI :: E Int f EI = 3::Int Should the inferred type be f :: E a -> a or f :: E a -> Int We can't tell, and neither is more general than the other. So GHC insists on knowing the result type. That's why you had to give the signature g::[()] in your example. So that's the story. If you find situations in which it's very hard to give a signature for the result type, I'd like to see them. Dimitrios has just written an Appendix to our ICFP paper about GADT inference, explaining the inference scheme -- it is not otherwise written up anywhere. I'll put it up shortly. Thanks Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Mitchell, Neil | Sent: 12 September 2008 13:51 | To: glasgow-haskell-users@haskell.org | Subject: GADT problems | | Hi | | The following code works in GHC 6.8.3, works in GHC 6.9.20071111, but | doesn't work in GHC HEAD. | | {-# 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) | | f (Foo GadtValue) = True | f _ = False | | Under GHC HEAD I get the error: | | GADT pattern match with non-rigid result type `t' | Solution: add a type signature | In the definition of `f': f (Foo GadtValue) = True | | Adding a type signature to f fixes this problem: | | f :: Foo -> Bool | | But I haven't found anywhere other than the top level f to add a type | signature. When the match is in a list comprehension, it becomes much | harder. While playing further I discovered this example: | | foos = undefined | g = [() | Foo GadtValue <- foos] | | This code doesn't compile under GHC HEAD, but does under 6.8.3. However, | adding the type signature: | | g :: [()] | | Makes the code compile. This is surprising, as [()] isn't a GADT type, | so shouldn't need stating explicitly. | | Any help on what these errors mean, or how they can be fixed with local | type annotations? | | 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
On Sun, Sep 14, 2008 at 7:11 AM, Simon Peyton-Jones
Neil
It's by design, and for (I think) good reason. GHC now enforces the rule that in a GADT pattern match - the type of the scrutinee must be rigid - the result type must be rigid - the type of any variable free in the case branch must be rigid
Here "rigid" means "fully known to the compiler, usually by way of a type signature". This rule is to make type inference simple and predictable -- it dramatically simplifies inference.
To see the issue, ask yourself what is the type of this function
data E a where EI :: E Int
f EI = 3::Int
Should the inferred type be f :: E a -> a or f :: E a -> Int We can't tell, and neither is more general than the other. So GHC insists on knowing the result type. That's why you had to give the signature g::[()] in your example.
So that's the story. If you find situations in which it's very hard to give a signature for the result type, I'd like to see them.
I find that usually when it becomes difficult is when I'm using existential types and lexically scoped type variables. I don't have an example ready but I could vaguely describe it. For example, using a case expression to pattern match on a constructor that has an existential type and also expecting part of the type of that expression to match a lexically scope type variable (I'm often also using phantom types, if that matters). In this case, I usually end up adding a where clause to specify the type signature while dancing around the other issues. It's typically not pretty but at the end of the day I've always been able to find a way to specify the type I need. Although, it does make me quite aware that GHC could report the type errors better when dealing with phantom types that are bound to an existential type. If you have multiple such phantoms as part of the type it can be quite confusing to figure out which ones the type checker isn't happy with. data Sealed a where Sealed :: a x y -> Sealed a data Foo a x y where .... case sealedFoo where Sealed (Foo 4) -> ... If you get a type error in the above sometimes it's hard to figure out if it's happening with x or with y. Sometimes the type parameter name chosen doesn't give you a hint about which type parameter of Foo is not unifying. I wish I had a concrete example to show you. I guess the next time it shows up I should send it in. Thanks, Jason
| > So that's the story. If you find situations in which it's very hard to give a signature for | the result type, I'd like to see them. | | I find that usually when it becomes difficult is when I'm using | existential types and lexically scoped type variables. | ... | | I wish I had a concrete example to show you. I guess the next time it | shows up I should send it in. Yes, please do! I'm always interested in bad type error messages. S
Hi Simon, I appreciate that everything must be rigid, but am still confused. Given the following operation: op (Foo GadtValue) = () I can add a top-level type signature, and it works: op :: Foo -> () But just putting those same type annotations in the actual function doesn't work: op (Foo GadtValue :: Foo) = () :: () From a simple point of view those two functions seem to have the same amount of type information, but GHC gives different behaviour. 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. Thanks Neil
-----Original Message----- From: Simon Peyton-Jones [mailto:simonpj@microsoft.com] Sent: 14 September 2008 3:11 pm To: Mitchell, Neil; glasgow-haskell-users@haskell.org Subject: RE: GADT problems
Neil
It's by design, and for (I think) good reason. GHC now enforces the rule that in a GADT pattern match - the type of the scrutinee must be rigid - the result type must be rigid - the type of any variable free in the case branch must be rigid
Here "rigid" means "fully known to the compiler, usually by way of a type signature". This rule is to make type inference simple and predictable -- it dramatically simplifies inference.
To see the issue, ask yourself what is the type of this function
data E a where EI :: E Int
f EI = 3::Int
Should the inferred type be f :: E a -> a or f :: E a -> Int We can't tell, and neither is more general than the other. So GHC insists on knowing the result type. That's why you had to give the signature g::[()] in your example.
So that's the story. If you find situations in which it's very hard to give a signature for the result type, I'd like to see them.
Dimitrios has just written an Appendix to our ICFP paper about GADT inference, explaining the inference scheme -- it is not otherwise written up anywhere. I'll put it up shortly.
Thanks
Simon
| -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org | [mailto:glasgow-haskell- users-bounces@haskell.org] On Behalf Of | Mitchell, Neil | Sent: 12 September 2008 13:51 | To: glasgow-haskell-users@haskell.org | Subject: GADT problems | | Hi | | The following code works in GHC 6.8.3, works in GHC 6.9.20071111, but | doesn't work in GHC HEAD. | | {-# 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) | | f (Foo GadtValue) = True | f _ = False | | Under GHC HEAD I get the error: | | GADT pattern match with non-rigid result type `t' | Solution: add a type signature | In the definition of `f': f (Foo GadtValue) = True | | Adding a type signature to f fixes this problem: | | f :: Foo -> Bool | | But I haven't found anywhere other than the top level f to add a type | signature. When the match is in a list comprehension, it becomes much | harder. While playing further I discovered this example: | | foos = undefined | g = [() | Foo GadtValue <- foos] | | This code doesn't compile under GHC HEAD, but does under 6.8.3. | However, adding the type signature: | | g :: [()] | | Makes the code compile. This is surprising, as [()] isn't a GADT type, | so shouldn't need stating explicitly. | | Any help on what these errors mean, or how they can be fixed with | local type annotations? | | 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
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
| I appreciate that everything must be rigid, but am still confused. Given | the following operation: | | op (Foo GadtValue) = () | | I can add a top-level type signature, and it works: | | op :: Foo -> () | | But just putting those same type annotations in the actual function | doesn't work: | | 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". | 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? Simon
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 <something>. I then replaced Int with <something> 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 ==============================================================================
| > | 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. Great. Now you can help me! Look at the documentation here http://www.haskell.org/ghc/dist/current/docs/users_guide/data-type-extension... The last bullet. What could I add that would eliminate your misunderstanding? You are in the ideal position to suggest concrete wording, because you know the problem and the solution. Examples are fine. Thanks | > 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. The error message here is: GADT pattern match in non-rigid context for `GadtValue' Solution: add a type signature In the pattern: GadtValue _ In the pattern: Foo (GadtValue _) In a stmt of a list comprehension: Foo (GadtValue _) <- undefined And indeed, the type of 'undefined' (which is the scrutinee of this particular pattern match) is forall a. a. Very non-rigid! You need a type signature for the scrutinee. For example, this works: g :: [()] g = [() | Foo (GadtValue _) <- undefined :: [Foo (E ())]] Does that help? Again, what words would help in the user manual. Simon
Hi
| 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.
Great. Now you can help me! Look at the documentation here http://www.haskell.org/ghc/dist/current/docs/users_guide/data- type-extensions.html#gadt The last bullet.
What could I add that would eliminate your misunderstanding? You are in the ideal position to suggest concrete wording, because you know the problem and the solution. Examples are fine.
My mistunderstanding stems from: (case undefined of Foo GadtValue -> ()) :: () -- is rigid (case undefined of Foo GadtValue -> () :: ()) -- not rigid The wording in the user manual is perfectly correct, but my intuition of how rigidity propogates was wrong. I'm also still not sure how the scrutinee (undefined in this case) is rigid, when in your response you said undefined was very non-rigid. An example in the user manual would be good, but having the compiler identify where the missing type signature is would be significantly better (albeit significantly more work). The example that would have helped me is: Given the case expression: case scrutinee of GadtConstructor variable -> result The potential type signatures that may be required to ensure rigidity are: (case scrutinee :: t of GadtConstructor (variable :: t) -> result) :: t
You need a type signature for the scrutinee. For example, this works:
g :: [()] g = [() | Foo (GadtValue _) <- undefined :: [Foo (E ())]]
Does that help? Again, what words would help in the user manual.
In this particular case I don't fully understand the implications, because the example is fake. If I encounter these issues in real code, I'll take another look. Thanks Neil ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
| > What could I add that would eliminate your misunderstanding? | > You are in the ideal position to suggest concrete wording, | > because you know the problem and the solution. Examples are fine. | | My mistunderstanding stems from: | | (case undefined of Foo GadtValue -> ()) :: () -- is rigid | | (case undefined of Foo GadtValue -> () :: ()) -- not rigid No, the former isn't rigid either. BOTH the scrutinee AND the return type must be rigid, and in the former case the scrutinee does not have a rigid type. | I'm also still not sure how the scrutinee (undefined in this case) is | rigid, when in your response you said undefined was very non-rigid. Quite right. See my comment above. | An example in the user manual would be good, but having the compiler | identify where the missing type signature is would be significantly | better (albeit significantly more work). The example that would have | helped me is: | | Given the case expression: | | case scrutinee of | GadtConstructor variable -> result | | The potential type signatures that may be required to ensure rigidity | are: | | (case scrutinee :: t of | GadtConstructor (variable :: t) -> result) :: t OK. Can you give a sample program and the error message you'd like to see? If you can suggest improvements to the manual I'm all ears. Notably, it says nothing about what "rigid" means or how it propagates. Simon
| My mistunderstanding stems from: | | (case undefined of Foo GadtValue -> ()) :: () -- is rigid | | (case undefined of Foo GadtValue -> () :: ()) -- not rigid
No, the former isn't rigid either. BOTH the scrutinee AND the return type must be rigid, and in the former case the scrutinee does not have a rigid type.
But the first compiles fine, so it seems that the scrutinee doesn't have to always be rigid?
| An example in the user manual would be good, but having the compiler | identify where the missing type signature is would be significantly | better (albeit significantly more work). The example that would have | helped me is: | | Given the case expression: | | case scrutinee of | GadtConstructor variable -> result | | The potential type signatures that may be required to ensure rigidity | are: | | (case scrutinee :: t of | GadtConstructor (variable :: t) -> result) :: t
OK. Can you give a sample program and the error message you'd like to see?
Given the program: g = case undefined of Foo GadtValue -> () I get the error message: Test.hs:13:12: GADT pattern match with non-rigid result type `t' Solution: add a type signature In a case alternative: Foo GadtValue -> () In the expression: case undefined of { Foo GadtValue -> () } In the definition of `g': g = case undefined of { Foo GadtValue -> () } Which last week I was reading as "add a type signature to Foo GadtValue -> ()". A better hint would be: Solution: add a type signature, probably at _TYPE_ (case undefined of { Foo GadtValue -> () }) :: _TYPE_
If you can suggest improvements to the manual I'm all ears. Notably, it says nothing about what "rigid" means or how it propagates.
I think the manual should give a conservative approximation of where type signatures should go -- i.e. if you put type signatures in all these places it will work. Details such as what rigid means or propagation rules are too unnecessary. My example in my previous mail would have helped me. Thanks Neil ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
| > | (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? Simon $ ghc-6.8.3 -c Neil.hs Neil.hs:17:12: GADT pattern match in non-rigid context for `GadtValue' Solution: add a type signature In the pattern: GadtValue In the pattern: Foo GadtValue In a case alternative: Foo GadtValue -> () bash-3.2$ ~/builds-04/validate-HEAD/ghc/stage1-inplace/ghc -c Neil.hs Neil.hs:17:12: GADT pattern match in non-rigid context for `GadtValue' Solution: add a type signature In the pattern: GadtValue In the pattern: Foo GadtValue In a case alternative: Foo GadtValue -> () bash-3.2$ {-# 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 :: Int -> () g x = case undefined of Foo GadtValue -> ()
| > | (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 ==============================================================================
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:neil.mitchell.2@credit-suisse.com] | 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 | ============================================================================== |
[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
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 ==============================================================================
On Mon, Sep 15, 2008 at 4:18 AM, Simon Peyton-Jones
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
participants (4)
-
Jason Dagit -
Mitchell, Neil -
Philippa Cowderoy -
Simon Peyton-Jones