Allow synonyms in some instance heads?

[garyb]

I think there may be two places where it may be reasonable to accept synonyms in instance heads:

1. If the synonym is being applied to a type
2. If the class variable is fully determined by another

I have a case where both these conditions coincide:

type Cursor = Mu CursorF

newtype X = X (Cofree MyF Cursor)

instance recursiveX ∷ Recursive X (EnvT (Mu CursorF) MyF) where ...

So here I have to use Mu CursorF in recursiveX, but with either of the rules above I'd be able to use Cursor in there instead.

The main reason we don't allow synonyms in instances is so there's no confusion if people try to do that directly for a type rather than using newtype, right? If so, I think the above cases still preserve that, and make some fancier use cases more convenient.

Thoughts?

[LiamGoodacre]

I would be happy with (2) :)
I haven't fully understood what (1) means - are you saying synonyms could be allowed under a type constructor? (In this case, under EnvT)

[garyb]

Yep, that's a better way of putting it!

[paf31]

I'm in favor of allowing instances for fully-applied synonyms, but I'm not sure if the functional dependency rule makes sense, since we can't guarantee everything will be fully applied after solving:

class WithDep a b | a -> b where
  withDep :: Proxy1 a -> Proxy1 b

type A a = Either a String

instance example :: WithDep (Either String) A where
  withDep Proxy1 = Proxy1

Here, we've somehow created a proxy for the type level function Λa. Either a String, right?

[garyb]

Using A like that wouldn't be allowed though? In that it falls foul of the no-partially-applied-synonyms rule.

[paf31]

Ok, then I don't understand (1). I agree that synonyms must be fully applied in any case.

[garyb]

1 would be something like:

Take these:

type T = X String
data F a

Disallow this, because it's making an instance "directly" for a synonym:

instance thing :: C T where ...

Allow this:

instance thing :: C (F T) where ...

As F itself is not a synonym.

It's the kind of instance that you'd probably rarely need to make except in a multiparam fundep-like situation anyway, as FlexibleInstance style instances are always a little suspect.

[paf31]

Actually, I think we should either allow neither or both of these. If we allow both, it would be because the synonym is fully applied in both cases, but the user would need to understand that it's just a shorthand, and not changing the behavior of the solver at all.

[garyb]

Yeah, and that's my worry - as if you allow C T then the (very common) mistake people make by trying to declare instances for synonyms of records will result in an error message that isn't very obvious. Perhaps we could tag it with a hint or something to resolve that case though?