[Haskell-cafe] Strange type error with associated type synonyms

[Claus Reinke]

> Basically, type checking proceeds in one of two modes: inferring or  
> checking.  The former is when there is no signature is given; the  
> latter, if there is a user-supplied signature.  GHC can infer  
> ambiguous signatures, but it cannot check them.  This is of course  
> very confusing and we need to fix this (by preventing GHC from  
> inferring ambiguous signatures).  The issue is also discussed in the  
> mailing list thread I cited in my previous reply.

As the error message demonstrates, the inferred type is not
correctly represented - GHC doesn't really infer an ambiguous
type, it infers a type with a specific idea of what the type variable
should match. Representing that as an unconstrained forall-ed 
type variable just doesn't seem accurate (as the unconstrained
type variable won't match the internal type variable) and it is this
misrepresentation of the inferred type that leads to the ambiguity.

Here is a variation to make this point clearer:

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}

class Fun d where
    type Memo d :: * -> *
    abst :: (d -> a) -> Memo d a
    appl :: Memo d a -> (d -> a)

f = abst . appl

-- f' :: forall d a. (Fun d) => Memo d a -> Memo d a
f' = abst . (id :: (d->a)->(d->a)) . appl

There is a perfectly valid type signature for f', as given in 
comment, but GHCi gives an incorrect one (the same as for f):

*Main> :browse Main
class Fun d where
  abst :: (d -> a) -> Memo d a
  appl :: Memo d a -> d -> a
f :: (Fun d) => Memo d a -> Memo d a
f' :: (Fun d) => Memo d a -> Memo d a

What I suspect is that GHCi does infer the correct type, with
constrained 'd', but prints it incorrectly (no forall to indicate the
use of scoped variable). Perhaps GHCi should always indicate
in its type output which type variables have been unified with 
type variables that no longer occur in the output type (here the 
local 'd'). 

If ScopedTypeVariables are enabled, that might be done via 
explicit forall, if the internal type variable occurs in the source file 
(as for f' here). Otherwise, one might use type equalities. 

In other words, I'd expect :browse output more like this:

f :: forall a d. (Fun d, d~_d) => Memo d a -> Memo d a
f' :: forall a d. (Fun d) => Memo d a -> Memo d a

making the first signature obviously ambiguous, and the
second signature simply valid.

Claus