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