On Fri, Apr 5, 2013 at 6:32 AM, Dimitrios Vytiniotis
Hmm, no I don’t think that Flattening is a very serious problem:
Firstly, we can somehow get around that if we use implication constraints and higher-order flattening
variables. We have discussed that (but not implemented). For example.
forall a. F [a] ~ G Int
becomes:
forall a. fsk a ~ G Int
forall a. true => fsk a ~ F [a]
Secondly: flattening under a Forall is not terribly important, unless you have type families that dispatch on
polymorphic types, which is admittedly a rather rare case. We lose some completeness but that’s ok.
For me, a more serious problem are polymorphic RHS, which give rise to exactly the same problems for type
inference as impredicative polymorphism. For instance:
type instance F Int = forall a. a -> [a]
g :: F Int
g = undefined
main = g 3
Should this type check or not? And then all our discussions about impredicativity, explicit type applications etc become
relevant again.
I would expect a saturated type family application to be expanded right away so that g effectively has type forall a . a -> [a], as if in fact we had type FInt = forall a . -> [a]. As long as you stay away from inferring type constructors, I suspect you should be fine. -- Gaby