[Haskell-cafe] AT solution: rebinding >>= for restricted monads

[Nicolas Frisby]

On the FD impasse:

>
> Witness.hs:33:0:
>     Couldn't match expected type `m'' (a rigid variable)
>            against inferred type `RealWitness a a''
>       `m'' is bound by the type signature for `>>' at Witness.hs:11:29
>     When using functional dependencies to combine
>       Witness WitnessReally a b (RealWitness a b),
> (and a screenful more)
>
> Any suggestions?
>

What follows isn't so much a suggestion, but I think it's a
description of this error's origins.

Note that >>='s signature from the class declaration

> class Witness w a b m | w a b -> m, m -> w a b where
>     (>>=) :: (Witness w a a' m', Witness w a' b m'') => m' x -> (x -> m'' y) -> m y
>     (>>) ::  (Witness w a a' m', Witness w a' b m'') => m' x -> m'' y -> m y
>     f >> g = f >>= const g
>     private_return :: x -> m x
>     fail :: String -> m x
>

is "copied" to this instance declaration,

> instance Witness WitnessReally a b (RealWitness a b) where
>

so we have:

(>>=) :: ( Witness WitnessReally a a' m'
            , Witness WitnessReally a' b m''
            ) => m' x -> (x -> m'' y) -> (RealWitness a b) y

Now consider what the signature of >>= for this instance would be if
this "copy from the class to the instance" operation were savvy to our
plans:

(>>=) :: ( Witness WitnessReally a a' (RealWitness a a')
            , Witness WitnessReally a' b (RealWitness a' b)
            ) => (RealWitness a a') x -> (x -> (RealWitness a' b) y)
-> (RealWitness a b) y

This signature is what the FD analyzer determines. Our above error
arises because the actual signature of >>= has m' where the FDs
indicate we'll always have (RealWitness a a'). Does that seem
accurate? (I've put off actually looking at the GHC source for ages
now...)

In my opinion, this is reminiscent of some of the scoped-type variable
issues and notions (e.g. wobbly types). By the functional dependency
|w a b -> m|, we know that the m' and m'' in the signature of >>= will
be determined as some particular types (i.e. the class is a type
function from w a b to m), and we'd just like to refer to whatever
those types actually are as m' and m''. It seems the FD analyzer
determines for us what those particular types are, but then the
type-checker is unhappy that we're naming them m' and m'' when we
should know more about them (e.g. that they have a RealWitness tycon).
Unfortunately, we have no choice about the signature of >>= at the
instance declaration, since it's copied straight from the class
declaration. If m' and m'' were recognized as partially wobbly
variables, then maybe this wouldn't be a problem. Or maybe wobbly
types could be framed in terms of functional dependencies on a
non-method's signature?

(The rest might be off-topic.)

This situation also conjures up some of my own confusion about FDs,
the open world assumption, and "finalizing" a typeclass. One of my
main confusions with FDs is how they play with the open world
assumption.

Another confusion is that just because your instance declarations
satisfy the FDs of a class, they won't necessisarily allow the type
inference engine to act in accord to those FDs. Sometimes you have to
break a class's definition into ancillary classes, each with one of
the FDs you want and appropriate instance declarations to drive the
inference along those particular FDs. If you try to cram all of the
FDs into one set of instance declarations, they tend to choke the FD
analyzer. (I read FDs as "a b and c" determine "x y and z"; this is a
description of the class's membership, but the FD analysis takes place
on the instance declarations themselves and not necessarily the types
admitted to the class.)

Nick