Hi Iavor, Thanks for the remarks.
so there is really no way for GHC to figure out what is the intended value > for `a`. > Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`? -- Conal On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki <iavor.diatc...@gmail.com>wrote: > 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-users@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >> >> >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users