Hello Conal, The issue with your example is that it is ambiguous, so GHC can't figure out how to instantiate the use of `foo`. It might be easier to see why this is if you write it in this form:
> foo :: (F a ~ b) => b > foo = ... Now, we can see that only `b` appears on the RHS of the `=>`, so there is really no way for GHC to figure out what is the intended value for `a`. Replacing `a` with a concrete type (such as `Bool`) eliminates the problem, because now GHC does not need to come up with a value for `a`. Another way to eliminate the ambiguity would be if `F` was injective---then we'd know that `b` uniquely determines `a` so again there would be no ambiguity. If `F` is not injective, however, the only workaround would be to write the type in such a way that the function arguments appear in the signature directly (e.g., something like 'a -> F a' would be ok). -Iavor On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott <co...@conal.net> wrote: > I sometimes run into trouble with lack of injectivity for type families. > I'm trying to understand what's at the heart of these difficulties and > whether I can avoid them. Also, whether some of the obstacles could be > overcome with simple improvements to GHC. > > Here's a simple example: > > > {-# LANGUAGE TypeFamilies #-} > > > > type family F a > > > > foo :: F a > > foo = undefined > > > > bar :: F a > > bar = foo > > The error message: > > Couldn't match type `F a' with `F a1' > NB: `F' is a type function, and may not be injective > In the expression: foo > In an equation for `bar': bar = foo > > A terser (but perhaps subtler) example producing the same error: > > > baz :: F a > > baz = baz > > Replacing `a` with a monotype (e.g., `Bool`) eliminates the error. > > Does the difficulty here have to do with trying to *infer* the type and > then compare with the given one? Or is there an issue even with type > *checking* in such cases? > > Other insights welcome, as well as suggested work-arounds. > > I know about (injective) data families but don't want to lose the > convenience of type synonym families. > > Thanks, -- Conal > > > _______________________________________________ > Glasgow-haskell-users mailing list > glasgow-haskell-us...@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe