Bugs item #1179108, was opened at 2005-04-08 12:02 Message generated for change (Tracker Item Submitted) made by Item Submitter You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1179108&group_id=8032
Category: Compiler (Type checker) Group: 6.4 Status: Open Resolution: None Priority: 5 Submitted By: Bjorn Bringert (bring) Assigned to: Nobody/Anonymous (nobody) Summary: GADT - fundep interaction Initial Comment: GADTs and fundeps don't seem to interact in the way that I (perhaps naively) expect. I expected that for each case, the type variables would be instantiated according to the type of the constructors, and then the fundep would be used to figure out the result type. {-# OPTIONS_GHC -fglasgow-exts #-} data Succ n data Zero class Plus x y z | x y -> z instance Plus Zero x x instance Plus x y z => Plus (Succ x) y (Succ z) infixr 5 ::: data List :: * -> * -> * where Nil :: List a Zero (:::) :: a -> List a n -> List a (Succ n) append :: Plus x y z => List a x -> List a y -> List a z append Nil ys = ys append (x ::: xs) ys = x ::: append xs ys {- GHC 6.4 says: Couldn't match the rigid variable `y' against `Succ z' `y' is bound by the type signature for `append' Expected type: List a y Inferred type: List a (Succ z) In the expression: x ::: (append xs ys) In the definition of `append': append (x ::: xs) ys = x ::: (append xs ys) -} ---------------------------------------------------------------------- You can respond by visiting: https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1179108&group_id=8032 _______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs