apfelmus:
Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
Let's alpha-rename the signatures and use explicit foralls for
clarity:
foo :: forall a. Id a -> Id a
foo' :: forall b. Id b -> Id b
GHC will try to match (Id a) against (Id b). As Id is a type
synonym family, it would *not* be valid to derive (a ~ b) from
this. After all, Id could have the same result for different
argument types. (That's not the case for your one instance, but
maybe in another module, there are additional instances for Id,
where that is the case.)
While in general (Id a ~ Id b) -/-> (a ~ b) , parametricity makes
it "true" in the case of foo . For instance, let Id a ~ Int .
Then, the signature specializes to foo :: Int -> Int . But due to
parametricity, foo does not care at all what a is and will be
the very same function for every a with Id a ~ Int . In other
words, it's as if the type variable a is not in scope in the
definition of foo .
Be careful, Id is a type-indexed type family and *not* a parametric
type. Parametricity does not apply. For more details about the
situation with GADTs alone, see
Foundations for Structured Programming with GADTs. Patricia Johann
and Neil Ghani. Proceedings, Principles of Programming Languages 2008
(POPL'08).
In full System F , neither definition would be a problem since the
type a is an explicit parameter.
You can't generally translate type family/GADT programs into System
F. We proposed an extension of System F called System F_C(X); see our
TLDI'07 paper:
http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html
Manuel
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
