Unification in Typeclass Resolution

[re-xyr]

Say in type class resolution, we meet the following instance

instance FTrans {A B C} {{ab: F A B}} {{bc: F B C}} : F A C

and we have the resolution problem F X Y. In the description of the tabled typeclass resolution paper, it will generate two subgoals on this instance: F X ?M and F ?M Y.

However the ?M does not behave exactly like a metavariable. Namely, it can have multiple temporary [worse, may be not temporary because both solutions may be applicable to the remaining subgoal] solutions: if we have instances F X Z1 and F X Z2, then ?M equates to both in the resolution process.

Should we change how our metavariable works? Or should we use another kind of syntactic construct for this purpose?

[ice1000]

@re-xyr Imho instance search and implicit inference are different anyway, so I'll prefer using another construct

[re-xyr]

I have another problem: If we have a function f : {A B C : Set} {{I : K A B C}} -> ... and class K {A B : Set} {out C : Set} where out signs the lift of meta constraint (i.e, I will be resolved after A and B solved but will not wait for C), then the problem we need to resolve is F A B ?M where ?M meta. However this conflicts with the previous discussion that ?M should be a separate construct.

[re-xyr]

Maybe we should seriously consider adding most general unifiers...

[re-xyr]

I thought about what does it mean when an instance matches a problem (i.e. reduces the problem into zero or more subgoals). The type of the instance may contain [bound variables, free variables] (TODO: can it contain metavariables? I think we should prohibit this). The problem may contain [free variables, metavariables]. Note: here free variables includes references to defs. We say the instance matches the problem iff we can find a most general unifier that may contain both bound variables and metavariables, but not free variables.

instance FTrans {A B C} {{ab: F A B}} {{bc: F B C}} : F A C -- Bound A, C.
instance Fxy : F X Y -- Free X, Y.

Fxy does not match problem F Z1 Z2 because the most general unifier X -> Z1, Y -> Z2 contains free variables. FTrans however does match F Z1 Z2.

[ice1000]

How can the type of an instance to contain metavars?

[re-xyr]

Like if someone deliberately leaves holes in the type of their instance.

[ice1000]

Like if someone deliberately leaves holes in the type of their instance.

Then how are these instances tycked?

[ice1000]

Maybe we should seriously consider adding most general unifiers...

I agree. It is useful anyway

[ice1000]

Are you interested in implementing it?

[ice1000]

Maybe we can also implement RTT, making our type theory to some extent extensional...

[re-xyr]

Then how are these instances tycked?

Edge case alert:

class F (A : Set) {}
instance : F _ {}

[ice1000]

Then the instance should raise a type error saying that unsolved meta at location

[re-xyr]

Are you interested in implementing it?

Yes.

[ice1000]

Are you interested in implementing it?

Yes.

aya-prover/aya-prover-proto#503 when

[re-xyr]

Then the instance should raise a type error saying that unsolved meta at location

Because meta should be solved within the definition? btw, this is why I posted https://twitter.com/fun_ext/status/1401468891474268162

[ice1000]

Because meta should be solved within the definition?

I think so.

[re-xyr]

aya-prover/aya-prover-proto#503 when

I think its unrelated to most general unifiers but this weekend maybe

[ice1000]

Then the instance should raise a type error saying that unsolved meta at location

Because meta should be solved within the definition? btw, this is why I posted https://twitter.com/fun_ext/status/1401468891474268162

I suggest asking in AK's discord server. Have you joined it yet?

[ice1000]

aya-prover/aya-prover-proto#503 when

I think its unrelated to most general unifiers but this weekend maybe

Ik but I'm very looking forward to it

[re-xyr]

I suggest asking in AK's discord server. Have you joined it yet?

No. Could you invite me?

[ice1000]

I suggest asking in AK's discord server. Have you joined it yet?

No. Could you invite me?

https://discord.gg/89c3EXtx

[re-xyr]

I suggest asking in AK's discord server. Have you joined it yet?

I'm afraid of speaking in front of strange ppl. How should I ask a question?

[ice1000]

@re-xyr Just post in #general

[re-xyr]

I suggest just add this single restriction: No Unsolved Meta In Instance Type

[ice1000]

@re-xyr Yeah

[re-xyr]

But another problem: Should restriction be checked after checking the head or the body? If the head, then it won't be possible to write this perfectly reasonable instance

instance Add _ {
  _+_ (m n : Nat) => m +N n
}

If the body, then how should we typecheck

instance Add _ {
  _+_ (m n : Nat) => match m, n of
    zero, n => zero
    suc m, n => suc (m + n) -- This instance search how?
}

?

[re-xyr]

So maybe not "No Unsolved Meta In Instance Type", but "Ignore Instances With Unsolved Metas"?

[ice1000]

@re-xyr IMO this meta should be solved..

[re-xyr]

Basically we can accept only these two kinds of mappings: [meta in problem -> term in instance type, bound variable in instance type -> term in meta]. Maybe we can instead check if the final most general unifier only contains these two kinds of mappings and not worry about whether metas are present in instance types.