Are fundeps the right model at all?

[Tom Pledger]

Marcin 'Qrczak' Kowalczyk writes:
 > Mon, 8 Jan 2001 17:53:35 +1300, Tom Pledger <Tom.Pledger@peace.com> pisze:
 > 
 > >  > Having types with type variables which are never instantiated nor
 > >  > constrained should be equivalent to having ground types!
 > > 
 > > Do you have any examples of such a type variable in an instance decl?
 > 
 > Now I have a practical example where fundeps don't work and keys
 > would work - but the type variable is later instantiated.
 > 
 > Let's take Parsec from ghc's libraries which includes the following
 > (this is cut down):
 > 
 > data TokenParser = TokenParser {
 >     identifier :: Parser String,
 >     reserved   :: String -> Parser (),
 >     operator   :: Parser String,
 >     reservedOp :: String -> Parser (),
 >     parens     :: forall a. Parser a -> Parser a}
 > 
 > makeTokenParser:: LanguageDef -> TokenParser
 > 
 > I would like to express this "first-class module" in my records
 > proposal, to make it extensible (there can be different types similar
 > to TokenParser with similar fields and used polymorphically together
 > with TokenParser).
 > 
 > Each record field in my proposal induces a class:
 >     class Has_field r a | r -> a where
 >         get_field :: r -> a
 > 
 > The fundep, or something which allows to find the instance from the
 > type of the record only, is required to make this practical. A type
 > which includes Has_field r a in its context, and includes r but not a
 > in its body, is legal.
 > 
 > For non-polymorphic fields it works great. But parens cause trouble:
 >     instance Has_parens TokenParser (Parser a -> Parser a)
 > This instance is illegal because of the fundep. What it should mean is:
 >     instance Has_parens TokenParser (forall a. Parser a -> Parser a)
 > but this is not possible either.
 [...]

Hallo again.

The second instance decl expresses the situation better, because it's
faithful to the rank-2 polymorphism in TokenParser, i.e. the
requirement that the TokenParser constructor's 5th argument have a
type at *least* as general as forall a. Parser a -> Parser a.  The first instance decl 

Should we be able to put a local forall in an instance decl?

I suspect that we shouldn't in general, because it would cause leaks
in the rank-2 polymorphism restrictions.  For example:

    module MA where
    class C a where f :: () -> a -> ()

    module MB where
    import MA
    f' :: C a => a -> ()
    f' = f ()

    module MC where
    import MA
    instance C (forall a. a -> a) where f z g = if g True then g () else z

If any other module imports both MB and MC, the partial application of
f in MB will break the "maximal function application subexpressions
must include arguments for all rank-2 polymorphic parameters"
restriction.  (I don't actually know the purpose of this restriction
and its friends, but I'm sure there's a good reason for them.)

Trex avoids the question of field types in contexts, by using a Lacks
context which only mentions the row type and the label.  Is the
combination of Trex and newtype worth another look?  This sort of
thing:

    newtype T1 a = T1 {unT1 :: Rec (foo :: a)}
    newtype T2 a = T2 {unT2 :: Rec (foo :: a, bar :: a)}

Regards,
Tom