Hi. Consider for example an expression e0 like:<br><br> fst (True,e)<br><br>where e is any expression. <br><br>e0 should have type Bool IMHO irrespectively of the type of e. In Haskell<br>this is the case if e's type is monomorphic, or polymorphic, or<br>
constrained and there is a default in the current module that removes<br>the constraints. However, e0 is not type-correct if e has a<br>constrained type and the constraints are not subject to<br>defaulting. For example:<br>
<br> class O a where o::a <br> main = print $ fst(True,o) <br><br>generates a type error; in GHC:<br> <br> Ambiguous type variable `a' in the constraint:<br> `O a' arising from a use of `o' at ...<br> Probable fix: add a type signature that fixes these type variable(s)<br>
<br>A solution (that avoids type signatures) can be given as follows.<br><br>The type of f e, for f of type, say, K=>t'->t and e of type K'=> t'<br>should be:<br><br> K +_t K' => t (not K U K' => t)<br>
<br>where K +_t K' denotes the constraint-set obtained by adding from K'<br>only constraints with type variables reachable from t.<br><br>(A type variable is reachable if it appears in the same constraint as<br>
either a type variable free in the type, or another reachable type<br>variable.)<br><br>Comments? Does that need and deserve a proposal?<br><br>Cheers,<br><br>Carlos<br>