feat: implicit argument derivation by Kamirus · Pull Request #5966 · caffeinelabs/motoko

Kamirus · 2026-04-01T09:31:38Z

Summary

Part 1 of #5903 — implicit argument derivation only, without structural derivation (__record/__tuple combiners).

The compiler can now derive implicit arguments from functions that themselves have implicit parameters. For example, an implicit compare : ([Nat], [Nat]) -> Order is automatically derived from Array.compare<Nat> when Nat.compare is in scope.

Derivation works transitively (e.g. compare for [[Nat]] chains through Array.compare<[Nat]> → Array.compare<Nat> → Nat.compare)
Recursive derivation cycles are detected and handled via rec_bindings
Depth is bounded by --implicit-derivation-depth (default 100)
Refactored resolve_hole and disambiguate_resolutions to support the new derivation tiers while preserving existing direct-match behavior
Improved error messages: derivation failures report which inner implicits are missing and suggest imports

Structural derivation (__record/__tuple combiners for records and tuples) will follow in a separate PR on top of this one.

Allow the compiler to derive implicit arguments from functions that themselves have implicit parameters (e.g. `compare` for `[Nat]` from `Array.compare<Nat>` + `Nat.compare`). Works transitively and is depth-limited via `--implicit-derivation-depth`. Structural derivation (`__record`/`__tuple` combiners) will follow in a separate PR. Made-with: Cursor

Made-with: Cursor

github-actions · 2026-04-01T09:58:31Z

Comparing from 2248a05 to eb151d2:
In terms of gas, no changes are observed in 5 tests.
In terms of size, no changes are observed in 5 tests.

crusso

Some interim comments before GH loses them...

crusso · 2026-04-21T12:06:23Z

 let experimental_stable_memory = ref experimental_stable_memory_default
 let typechecker_combine_srcs = ref false (* useful for the language server *)
 let blob_import_placeholders = ref false (* when enabled, blob:file imports resolve as empty blobs *)
+let implicit_derivation_depth = ref 100


I guess this will affect all imported code too. Maybe that's ok but seems fragile.

yes, but we don't have flags per file/package and we need some default cap

crusso · 2026-04-22T08:57:42Z

+     Shared and Composite functions (actors, async) are excluded
+     since implicits are a local-scope, synchronous mechanism. *)
+  let is_matching_typ_with_holes hole candidate_typ =
+    match T.promote hole.hole_typ, T.promote candidate_typ with


match T.promote hole.hole_typ, T.promote candidate_typ with

I'm not sure you should promote the type of the hole, only the candidate. If this was a variable, it would replace it by its bounds (in what I think is a negative position). Suppose we had a hole of type T <: U and a candidate of type U. Then U <: T only if we substitute U for T. But we could actually substitute any W < U (strictly less than) for T too.

good catch!

I'll see if I can construct a counter-example...

... Hmm, not having much luck.

crusso · 2026-04-24T15:34:23Z

+     since implicits are a local-scope, synchronous mechanism. *)
+  let is_matching_typ_with_holes hole candidate_typ =
+    match T.promote hole.hole_typ, T.promote candidate_typ with
+    | T.Func (T.Local, T.Returns, [], req_args, req_rets),


Is there any reason the hole type can't be a generic function - this seems to require the hole to be non-generic and I guess the witness to be monomorphic? I guess we could extend later if need.

I guess it's just because we don't support inference for unannotated generic lambdas, right?

Indeed, this requires the hole to have a function type, though we don't require this elsewhere. That's what tripped me up in #6054.

I guess this approach of inserting implicit arguments is needed to make the existing (flattened) Array.compare work without changes to core.

Another option might be to look for curried applications that produce the desired hole type directly, and then extend, e.g., core Array with:

// existing Array.compare public func compare<T>(a1 : [T], a2 : [T], compare : (T, T) -> Order) : Order { ... }; // derivation oublic func deriveCompare<A>(compareA : (implicit : (compare : T -> T -> Order))) : (compare : ([T], [T]) -> Order)) = func( a1, a2) { compare( a1, a2, compareA) };

Then our witnesses are not lambdas that insert arguments but partial applications of functions that only take implicit arguments and produce a matching witness (without constraining the dictionary type to be a function),

Then the search for derivations only considers functions with (exlusively) implicit arguments that produces
a matching type.

But maybe our bimatch is not up to that or this winds up requiring backtracking.

It also means we would need to add some bindings to core to derive compare, eq and toText for generic containers, instead of it just working with our existing core.

Is there any reason the hole type can't be a generic function

No, just simplicity, we can extend if we ever need that

I guess this approach of inserting implicit arguments is needed to make the existing (flattened) Array.compare work without changes to core.

Not only that, see #5966 (comment)

crusso · 2026-04-24T21:45:01Z

+
+### Implicit derivation
+
+When no direct match exists, the compiler can **derive** an implicit argument from a function that itself has implicit parameters. This eliminates the need for boilerplate wrapper functions. The candidate function can be polymorphic (the compiler infers the type instantiation) or monomorphic.


I don't think anything here clearly states that the hole must have a (monomorphic) function type although perhaps its implied by saying that stripping the implicit arguments from the candidate produces a matching type.

I now realize that's probably why my example in #6054 fails.

I've explored this extension in #5991 (see comments there)
but this approach of deriving values (records/modules with funcs) instead of funcs is weaker, as it does not extend to __record to allow generic folds over records/tuples/etc
We could have both but this complicates the PR even more
So I'd just refactor your example to have two separate implicits, instead of a single record that ships both
This approach is simpler and extends to __record.
I'd just define toCandid and fromCandid separately instead of rep.

btw, if you want to allow context-dot syntax like myObj.toCandid() then you'd need an indirection like

func toCandid<A>(self : A, toCandidImpl : (implicit : A -> Blob)) : Blob { toCandidImpl(self) }

crusso · 2026-04-27T17:44:23Z

+ 31 │  ignore needsCompare([1], [2]); // Array.compare is unique head, but inner Nat compare is ambiguous
+    │         ^^^^^^^^^^^^^^^^^^^^^^ 
+    = note: Implicit derivation failed:
+                 `compare : (Nat, Nat) -> Order` ambiguous: `MyNat.compare`, `Nat.compare`


Suggested change

`compare : (Nat, Nat) -> Order` ambiguous: `MyNat.compare`, `Nat.compare`

`compare : (Nat, Nat) -> Order` has ambiguous solutions: `MyNat.compare`, `Nat.compare`

Might be clearer.

crusso · 2026-04-27T17:46:25Z

+        Format.asprintf env "`%s : %a` not found"
+          name display_typ_oneline typ :: acc)
+    | HoleAmbiguous ambiguous_candidates ->
+      Format.asprintf env "`%s : %a` ambiguous: %s"


Suggested change

Format.asprintf env "`%s : %a` ambiguous: %s"

Format.asprintf env "`%s : %a` has ambiguous solutions: %s"

Kamirus requested a review from a team as a code owner April 1, 2026 09:31

Kamirus force-pushed the kamil/implicit-derivation-pt1 branch from 5090a10 to b2eb1ee Compare April 1, 2026 09:32

Kamirus force-pushed the kamil/implicit-derivation-pt1 branch from b2eb1ee to 7d14732 Compare April 1, 2026 09:34

a

13fddcf

Made-with: Cursor

Kamirus force-pushed the kamil/implicit-derivation-pt1 branch from 6afe071 to 13fddcf Compare April 1, 2026 09:37

Kamirus requested review from christoph-dfinity and crusso April 1, 2026 09:41

Kamirus changed the title ~~feat: implicit argument derivation (pt 1 of #5903)~~ feat: implicit argument derivation Apr 1, 2026

Kamirus and others added 5 commits April 2, 2026 11:12

removes rename hints for implicit errors

d33207c

Merge branch 'master' into kamil/implicit-derivation-pt1

5689c5f

format

e86c6bb

Merge branch 'master' into kamil/implicit-derivation-pt1

065b517

Merge branch 'master' into kamil/implicit-derivation-pt1

59987b8

Kamirus mentioned this pull request Apr 13, 2026

experiment: Structural comparison #5841

Closed

Merge branch 'master' into kamil/implicit-derivation-pt1

9b961a3

crusso reviewed Apr 22, 2026

View reviewed changes

Merge branch 'master' into kamil/implicit-derivation-pt1

eb151d2

crusso reviewed Apr 24, 2026

View reviewed changes

Comment thread src/mo_frontend/typing.ml

crusso reviewed Apr 24, 2026

View reviewed changes

crusso mentioned this pull request Apr 24, 2026

experiment: implicit-derivation-rep example of type reps failing inference #6054

Draft

crusso reviewed Apr 24, 2026

View reviewed changes

review

76f82af

crusso reviewed Apr 27, 2026

View reviewed changes

crusso mentioned this pull request Apr 27, 2026

feat: implicit argument derivation and structural record synthesis #5903

Open


		### Implicit derivation

		When no direct match exists, the compiler can derive an implicit argument from a function that itself has implicit parameters. This eliminates the need for boilerplate wrapper functions. The candidate function can be polymorphic (the compiler infers the type instantiation) or monomorphic.

	`compare : (Nat, Nat) -> Order` ambiguous: `MyNat.compare`, `Nat.compare`
	`compare : (Nat, Nat) -> Order` has ambiguous solutions: `MyNat.compare`, `Nat.compare`

	Format.asprintf env "`%s : %a` ambiguous: %s"
	Format.asprintf env "`%s : %a` has ambiguous solutions: %s"

Conversation

Kamirus commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Uh oh!

github-actions Bot commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

crusso left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

crusso Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Kamirus Apr 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Kamirus commented Apr 1, 2026 •

edited

Loading

github-actions Bot commented Apr 1, 2026 •

edited

Loading

crusso Apr 24, 2026 •

edited

Loading

Kamirus Apr 27, 2026 •

edited

Loading