Motivation: make sure the behavior is consistent with other arithmetic
operators.
This commit also removes the instance
```
instance : HMod (Fin n) Nat (Fin n) where
hMod := Fin.modn
```
because we have a coercion from `Fin n` to `Nat`.
Thus, given `a : Fin n` and `b : Nat`, `a % b` is ambiguous.
In order to guarantee termination of type class synthesis when resolving
coercions, a good rule of thumb is that the instances should not
introduce metavariables (during TC synthesis). For common coercion type
classes this means:
- `Coe T S`, `CoeTail T S`: the variables of `T` must be a subset of those of `S`
- `CoeHead T S`: the variables of `S` must be a subset of those of `T`
If these rules are not followed, we can easily get nontermination. In
this case: `CoeTC Foo Syntax` is reduced to `CoeTC Foo (TSyntax ?m_1)`
using the (dangerous) `Coe (TSyntax k) Syntax` instance, to which we can
then apply the otherwise fine `Coe (TSyntax [k]) (TSyntax (k'::ks))`
coercion infinitely often.
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818
Type class resolution was diverging when trying to synthesize
```lean
HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
```
and Lean was diverging while unfolding
```lean
instance : OfScientific Float where
ofScientific m s e :=
if s then
let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
let m := (m <<< (3 * e + s)) / 5^e
Float.ofBinaryScientific m (-4 * e - s)
else
Float.ofBinaryScientific (m * 5^e) e
```
was being unfolded.
Anothe potential solution for the problem above is to erase the
`optParam` annotations before performing type class resolution.
Most notable change: `Quote` is now parameterized by the target kind.
Which means that `Name` etc. could actually have different
implementations for quoting into `term` and `level`, if that need ever
arises.
