order of arguments matters
Why does only tr2 work, although the only difference between tr1 and tr2 is the order of arguments? import Data.Tree (Tree(..)) data Type a where Tree :: Type a -> Type (Tree a) Int :: Type Int String :: Type String type Traversal1 = forall a.a -> Type a -> a type Traversal2 = forall a.Type a -> a -> a tr1 :: Traversal1 tr1 (Node _ (t:_)) (Tree Int) = Node 1 [t] tr1 n Int = n+n tr1 s String = s++s tr2 :: Traversal2 tr2 (Tree Int) (Node _ (t:_)) = Node 1 [t] tr2 Int n = n+n tr2 String s = s++s Couldn't match expected type `a' against inferred type `Tree Int' `a' is a rigid type variable bound by the type signature for `tr1' at tratest.hs:9:25 In the pattern: Node _ (t : _) In the definition of `tr1': tr1 (Node _ (t : _)) (Tree Int) = Node 1 [t]
I believe this is caused by type equalities that are introduced by the Type a argument. In tr2 you get something like a ~ Int or a ~ String, allowing the function to type check. In tr1 that equality is never introduced so the type checker thinks a and Int are distinct types. But I'm sure someone else can provide a better (more correct) explanation.
I checked out the GHC documentation on the GADTs extension [1]: "The key point about GADTs is that pattern matching causes type refinement." So in tr2 (Tree Int) (Node _ (t:_)) = Node 1 [t] the 'a' in 'Type a' is refined to 'Type (Tree a)'. But in tr1 (Node _ (t:_)) (Tree Int) = Node 1 [t] you want to "generalise" the type 'Tree a' to 'Type (Tree a)', which is not possible. 1 - http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/data-type-extens...
participants (2)
-
Peter Padawitz -
Roel van Dijk