Remove explicitness information

[umazalakain]

Removes Kind.Explicitness, instead type variables are understood to be globally free, implicit, and for type inference to solve if they are not bound, and explicit otherwise. Type assertions are also removed, they are substituted with type annotations where the FTVs of the asserted type are preserved.

Plenty of tests don't pass, I need to figure out why.

[Bastacyclop]

I think that the preserve set should either be:

1. global to a rewritten expression:

val s = rewrite1 `;` rewrite2
val typed = start.toExpr
implicit val preserve = collectFreeEnv(typed)
s(typed) // uses 'preserve'

2. taken from the left-hand-side of each rewrite rule

def s: Strategy = lhs => infer(rhs :: lhs.t, collectFreeEnv(lhs), getFTVs(lhs))

Solution 2. requires less global code changes and is more similar to the solution I used in the equality saturation side:

shine/src/main/scala/rise/eqsat/NamedRewrite.scala

Lines 15 to 23 in 91a3d2a

	val (lhs, rhs) = rule
	val untypedFreeV = collectFreeEnv(lhs).map { case (name, t) =>
	assert(t == rct.TypePlaceholder)
	name -> rct.TypeIdentifier("t" + name)
	}
	val typedLhs = preservingWithEnv(lhs, untypedFreeV, Set())
	val freeV = collectFreeEnv(typedLhs)
	val (_, freeT) = rise.core.IsClosedForm.freeVars(typedLhs)
	val typedRhs = preservingWithEnv(rc.TypeAnnotation(rhs, typedLhs.t), freeV, freeT)

In the future we can also consider having a common syntax for both equality saturation and Elevate rewrite rules:

def etaAbstraction = f : (a -> b) --> λx. (f x)
def etaReduction = λx. (f x) --> f
  when f ∌ x // x not in freeVars(f)

def mapFusion = map f (map g in) --> map λx. (f (g x)) in
def mapFission = {dt: data} -> map λx. (f (gx : dt)))) --> λin. map f (map λx. gx in)
  when f ∌ x

This would also enable type-checking Elevate rewrite rules ahead of match like I do for eqsat rewrite rules.

@michel-steuwer

[umazalakain]

Pushed something along this lines, thanks!

[Bastacyclop]

this results in DataTypeIdentifier("s") == NatIdentifier("s")?

[Bastacyclop]

do we properly deal with such dependent types when collecting free variables?

[umazalakain]

I think so, IsClosedForm deals with NatToDataLambdas

[umazalakain]

Making a more self-contained PR in #174