question about GADT's and error messages

[Daniel Wagner]

I just hit a similar error the other day. I think the gist of it is that 
there are two perfectly good types, and neither is more general than the 
other. A slightly different example shows why more clearly:

foo (AInt i) = (3 :: Int)

Now, what type should this have?

foo :: Any a -> a
foo :: Any a -> Int

both seem pretty good, and neither is clearly better. It's not *as* 
obvious what the two candidates might be for your example, but maybe you 
could imagine something like these two types:

demo1 :: AInt a -> IO ()
type family Foo a
type instance Foo Int = IO ()
demo1 :: AInt a -> Foo a

Again, not too clear that one is better, I think.
~d

On 2014-05-13 14:20, S. Doaitse Swierstra wrote:
> Given the following code:
> 
> {-# LANGUAGE GADTs #-}
> data Any a where
> AInt :: Int -> Any Int
> 
> -- demo 1 does not compile
> {-
> demo1 a = do case a of
>             (AInt i) -> print i
> 
>  Couldn't match expected type ‘t’ with actual type ‘IO ()’
>    ‘t’ is untouchable
>      inside the constraints (t1 ~ Int)
>      bound by a pattern with constructor
>                 AInt :: Int -> Any Int,
>               in a case alternative
>      at /Users/doaitse/TryHaskell/TestGADT.hs:6:17-22
>    ‘t’ is a rigid type variable bound by
>        the inferred type of demo1 :: Any t1 -> t
>        at /Users/doaitse/TryHaskell/TestGADT.hs:5:1
>  Relevant bindings include
>    demo1 :: Any t1 -> t
>      (bound at /Users/doaitse/TryHaskell/TestGADT.hs:5:1)
>  In the expression: print i
>  In a case alternative: (AInt i) -> print i
> Failed, modules loaded: none.
> -}
> 
> 
> -- all the following go through without complaints:
> 
> a = AInt 3
> demo2 = do case a of
>             (AInt i) -> print i
> 
> demo3 :: IO ()
> demo3 = do case a of
>             (AInt i) -> print i
> 
> 
> demo4 = do case AInt 3 of
>             (AInt i) -> print i
> 
> demo5 :: Any Int -> IO ()
> demo5 a = do case a of
>             (AInt i) -> print i
> 
> I do not see why the error message in demo1 arises. It claims it can't
> match some t with the type IO (), but when I tell that the result is
> IO () it can?
> I think at least the error message is confusing, and not very helpful.
> I would have in no way been able to get the clue that add a type
> signature as in the case of demo5 would solve the problem.
> 
> What am I overlooking?
> 
> Doaitse
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users