[Haskell-cafe] Reachable variables exercise

[Luke Palmer]

I am not totally sure if I understand your proposal correctly, but if
I do, then it has a flaw.  Consider:

    class Boolable a where
        boolify :: a -> Bool

    class O a where
        o :: a

    main = print $ boolify o

It seems like under your proposal this should not be a type error.
But if that is so, then what is its output?

Luke

On Thu, Sep 16, 2010 at 7:31 AM, Carlos Camarao
<carlos.camarao at 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>