## Expand Backpack's signature matching relation beyond definitional equality

Currently, signature matching is done by strict definitional equality. This can be pretty inconvenient in some cases (it is also the only place in the Haskell language that we actually expose definitional equality):

- *Polymorphism.** This is the obvious one. If I have an implementing function that is more polymorphic than my signature, I have to manually monomorphize it.

```
unit p where
signature H where
import Prelude (Int)
data String
length :: String -> Int
unit q where
module H(String, length) where
-- from Prelude
unit r where
dependency p[H=q:H]
```

Gives

```
<no location info>: error:
Identifier ‘Data.Foldable.length’ has conflicting definitions in the module
and its hsig file
Main module: Data.Foldable.length ::
Data.Foldable.Foldable t => forall a. t a -> GHC.Types.Int
Hsig file: Data.Foldable.length ::
GHC.Base.String -> GHC.Types.Int
The two types are different
```

Essentially, you have to monomorphize any functions you want to use. Annoying!

One particular place this shows up is if you're incrementally Backpack'ing an interface that has an existing type class. In this case, you might like to just reexport the methods of the type class and "fill" the imports; but these methods have the wrong types! (They're not monomorphic enough).

- *Quantifier ordering.** Here's a more subtle one: if I don't explicitly specify a type signature, GHC will pick whatever quantifier ordering it wants. Quantifier ordering affects definitional equality.

It's actually pretty easy to trigger this, since GHC seems to always pick the reverse of what you'd get if you explicitly specified the type signature:

```
unit p where
signature H where
k :: a -> b -> a
unit q where
module H where
k x y = x
unit r where
dependency p[H=q:H]
```

Fails with:

```
q.bkp:7:9: error:
Identifier ‘q:H.k’ has conflicting definitions in the module
and its hsig file
Main module: q:H.k :: t2 -> t1 -> t2
Hsig file: q:H.k :: a -> b -> a
The two types are different
```

- *Constraint relaxation.** In #12679 (closed), you might want to define an abstract class which you can use to let implementors pass in type class instances that they might need. But you often end up in situations where the real implementations of your functions require less constraint than the signature specifies; for example, you might write
`insert :: Key k => k -> a -> Map k a -> Map k a`

, but if Map is an association list and just appends the new value onto the front of the list, no Eq constraint needed! There goes another impedance matching binding. - *Type families.** Type family applications aren't reduced when deciding definitional equality.

```
{-# LANGUAGE TypeFamilies #-}
unit p where
signature H where
f :: Int
unit q where
module H where
type family F
type instance F = Int
f :: F
f = 2
unit r where
dependency p[H=q:H]
```

Gives

```
q.bkp:11:9: error:
Identifier ‘q:H.f’ has conflicting definitions in the module
and its hsig file
Main module: q:H.f :: q:H.F
Hsig file: q:H.f :: GHC.Types.Int
The two types are different
```

- *Discussion.** It's instructive to consider what the impacts of this sort of relaxation would have on hs-boot files. Some of the equalities that users expect in the source language have operational impact: for example, the ordering of constraints affects the calling convention of the function in question. So there would need to be an impedance matching binding to reorder/drop constraints to match the defining function. We already do an impedance matching of this sort with dictionary functions; this would be a logical extension. Thus, a signature would have to monomorphize, coerce, etc--whatever it needs to show the matching holds. I think this is quite plausible, although it would require rewriting this chunk of code.