> In my case, we had rigid type signatures all over the place. The > wiki document says that the type must be rigid at the point of the > match. I guess that's what we were violating. If the code I posted > isn't supposed to type check then I would like to report, as user > feedback, that GADTs have become unwieldy.
I'm now running into this problem big time on my existing test harness (I'd previously checked the main code and that worked - see http://www.haskell.org/pipermail/glasgow-haskell-users/2008-November/016160.html). > > I grant that it's less convenient than one would like. The > difficulty is that GADTs get you into territory where it's easy to > write programs that have multiple *incomparable* types. That is, > there is no "best" type (unlike Hindley-Milner). So we pretty much > have to ask the programmer to express the type. > > Once we are in that territory, we need to give simple rules that say > when a type signature is needed. I know that I have not yet found a > way to express these rules -- perhaps GHC's users can help. My > initial shot is > http://haskell.org/haskellwiki/Upgrading_packages%23Changes_to_GADT_matching#Changes_to_GADT_matching > > I couldn't figure out how to fix that code by just adding a type > signature. I've read this and I couldn't figure it out either. I've tried the heuristic and it works fine for some cases but not others: > arbitrarySeq :: Sequence a -> Gen RepSeqVal > arbitrarySeq Nil = > return (RepSeqVal Nil Empty) > arbitrarySeq (Cons (CTMandatory (NamedType n i t)) ts) = > do u <- arbitraryType t > us <- arbitrarySeq ts > case u of > RepTypeVal a v -> > case us of > RepSeqVal bs vs -> > return (RepSeqVal (Cons (CTMandatory (NamedType n i a)) bs) > (v:*:vs)) > QuickTest.lhs:240:13: > GADT pattern match in non-rigid context for `Nil' > Solution: add a type signature > In the pattern: Nil > In the definition of `arbitrarySeq': > arbitrarySeq Nil = return (RepSeqVal Nil Empty) > *Rename> :t Nil > Nil :: Sequence Nil So this fixes the first case: > arbitrarySeq :: Sequence a -> Gen RepSeqVal > arbitrarySeq (Nil :: Sequence Nil) = > return (RepSeqVal Nil Empty) But not the second case: > QuickTest.lhs:242:14: > GADT pattern match in non-rigid context for `Cons' > Solution: add a type signature > In the pattern: Cons (CTMandatory (NamedType n i t)) ts > In the definition of `arbitrarySeq': > arbitrarySeq (Cons (CTMandatory (NamedType n i t)) ts) > = do u <- arbitraryType t > us <- arbitrarySeq ts > case u of RepTypeVal a v -> ... And now I'm stuck: > *Rename> :t Cons > Cons :: ComponentType a -> Sequence l -> Sequence (a :*: l) What type should I give the Cons pattern? If I try the heuristic: > arbitrarySeq ((Cons (CTMandatory (NamedType n i t)) ts) :: Int) = the the compiler suggests > QuickTest.lhs:242:14: > Couldn't match expected type `Sequence a' > against inferred type `Int' but trying > arbitrarySeq ((Cons (CTMandatory (NamedType n i t)) ts) :: Sequence a) = gives > QuickTest.lhs:242:68: Not in scope: type variable `a' > > Did you try giving a type signature to the (entire) case expression, > as I suggested? That should do it. > I'm not sure what this means or how to do it. Can you give an example or is it buried in some earlier email? I will go and have another look. > I urge you to consider designing a modified or new syntactic form for > working with GADT pattern matches. The quasi-dependent typing that > GADTs give developers is very powerful and it would seem that GHC > Haskell with GADTs is as close to dependent typing that developers > writing "real-world" software can get. I know of no other production > ready compilers that provide dependent or close to dependent typing. > Dependent typing seems to be a growing area of interest. For these > reasons I think it's important for GHC to focus on making them > pleasanter to work with again; even if it means adding to the > language again. > > If I knew how to do that, I'd love to. Here's one idea you might not > like: restrict GADT matching to function definitions only (not case > expressions), and require a type signature for such pattern matches. > That wouldn't require adding new stuff. But GHC's current story is a > bit more flexible. > > I also feel that the type errors given when working with existential > types, especially GADTs with existentials, are confusing. I think I am using existential types to test GADT code. See http://www.haskell.org/haskellwiki/QuickCheck_/_GADT which no longer works with 6.10.1. > mostly because the types of the sub-expressions in the program are > not visible to the user. More introspection into the inferred types > would help users. I have some ideas on how to improve this, what the > output should look like and I would like to implement it too, but I > haven't had a chance to start a prototype yet. > > I agree they are confusing. I always encourage people to suggest > alternative wording for an error message that would make it less > confusing (leaving aside how feasible or otherwise it'd be to > generate such wording). So next time you are confused but figure it > out, do suggest an alternative. > > Thanks for helping. You can't develop a good user interface without > articulate and reflective users. Thanks. > _______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
