[Haskell-cafe] Re: checking types with type families

[Claus Reinke]

>  Prelude> :t id :: Eq b => b -> b
>  id :: Eq b => b -> b :: (Eq b) => b -> b
>  Prelude> id :: Eq b => b -> b
>
>  <interactive>:1:0:
>      No instance for (Show (b -> b))
>        arising from a use of `print' at <interactive>:1:0-19
>      Possible fix: add an instance declaration for (Show (b -> b))
>      In a stmt of a 'do' expression: print it
>
> The Eq constraint is irrelevant to the fact that there is no b -> b Show
> instance. The search for an instance looks only at the type part, and if 
> it
> finds a suitable match, then checks if the necessary constraints are also 
> in
> place.

Thanks - that first sentence is right, but not because of the second!-)

I thought the error message was misleading, speaking of instance
when it should have been speaking about instance *head*. But I
was really confused by the difference between (making the show
explicit and using scoped type variables):

    *Main> :t (show (id::a->a))::forall a.Eq a=>String

    <interactive>:1:0:
        Ambiguous constraint `Eq a'
            At least one of the forall'd type variables mentioned by the 
constraint
            must be reachable from the type after the '=>'
        In an expression type signature: forall a. (Eq a) => String
        In the expression:
              (show (id :: a -> a)) :: forall a. (Eq a) => String

    <interactive>:1:1:
        Could not deduce (Show (a -> a)) from the context (Eq a)
          arising from a use of `show' at <interactive>:1:1-15
        Possible fix:
          add (Show (a -> a)) to the context of an expression type signature
          or add an instance declaration for (Show (a -> a))
        In the expression:
              (show (id :: a -> a)) :: forall a. (Eq a) => String

which does list a non-empty context from which 'Show (a->a)'
could not be deduced and

    *Main> :t show (id :: Eq a => a-> a)

    <interactive>:1:0:
        No instance for (Show (a -> a))
          arising from a use of `show' at <interactive>:1:0-25
        Possible fix: add an instance declaration for (Show (a -> a))
        In the expression: show (id :: (Eq a) => a -> a)

which only talks about general 'Show (a->a)' instances. We
cannot define 'instance Show (forall a. Eq a=>a->a)', which
is why the 'Eq a' constraint plays no role, I think..

Btw, the issues in the other example can be made more
explicit by defining:

    class MyEq a b | a->b, b->a
    instance MyEq a a

First, both FDs and TFs simplify this:

    *Main> :t id :: (forall b. MyEq b Bool => b->b)
    id :: (forall b. MyEq b Bool => b->b) :: Bool -> Bool
    *Main> :t id :: (forall b. b~Bool => b->b)
    id :: (forall b. b~Bool => b->b) :: Bool -> Bool

but the FD version here typechecks (note, though, that the
type is only partially simplified)

    *Main> :t id :: (forall b. MyEq b Bool => b->b)
        -> (forall b. MyEq b Bool => b->b)
    id :: (forall b. MyEq b Bool => b->b)
        -> (forall b. MyEq b Bool => b->b)
      :: (forall b. (MyEq b Bool) => b -> b) -> Bool -> Bool

while the TF version doesn't

    *Main> :t id :: (forall b. b~Bool => b->b)
        -> (forall b. b~Bool => b->b)

    <interactive>:1:0:
        Couldn't match expected type `forall b. (b ~ Bool) => b -> b'
               against inferred type `forall b. (b ~ Bool) => b -> b'
          Expected type: forall b. (b ~ Bool) => b -> b
          Inferred type: forall b. (b ~ Bool) => b -> b
        In the expression:
              id ::
                (forall b. (b ~ Bool) => b -> b)
                -> (forall b. (b ~ Bool) => b -> b)

Claus