Implicit parameters for Unison — RFC + working prototype

[runarorama]

This PR proposes adding Scala-3-style implicit parameters (given / =>) to Unison and includes a working prototype. It exists to anchor RFC discussion: read the design, run the examples below, push back on anything that surprises you.

The end-to-end example from the design discussion typechecks, elaborates, runs, and round-trips through view:

class Monoid m = { op : m -> m -> m, zero : m }

given Monoid.nat : Monoid Nat = Monoid (Nat.+) 0

foldLeft : (b -> a -> b) -> b -> [a] -> b
foldLeft f z xs =
  match xs with
    [] -> z
    h +: t -> foldLeft f (f z h) t

foldMap : (Monoid m) => (a -> m) -> [a] -> m
foldMap f = foldLeft (acc a -> Monoid.op acc (f a)) Monoid.zero

foo : Nat
foo = foldMap Text.size ["one", "two", "three"]

> foo

UCM after add:

+ type Monoid m
+ foldLeft    : (b ->{g1} a ->{g} b) -> b -> [a] ->{g, g1} b
+ foldMap     : Monoid m => (a ->{g} m) -> [a] ->{g} m
+ foo         : Nat
+ Monoid.nat  : Monoid Nat
+ Monoid.op   : Monoid m => m -> m -> m
+ Monoid.zero : Monoid m => m

> foo
    ⧩
    11

A polymorphic-with-premise given also works end-to-end:

class Show s = { show : s -> Text }

given Show.nat : Show Nat = Show Nat.toText

given Show.list : forall a. Show a => Show [a] =
  Show (xs -> "[" ++ textJoin ", " (List.map Show.show xs) ++ "]")

foo : Text
foo = Show.show [1, 2, 3]

> foo
    ⧩
    "[1, 2, 3]"

Show.list's premise Show a is discharged against the function's own lexical => parameter while its body is checked, and at foo's call site the resolver chains Show.list (premise Show a) → Show.nat to build Show [Nat]. The chosen dictionaries are wired into foo's hash, and view foo round-trips to exactly what the user wrote.

dependencies foo lists Show.nat and Show.list — the resolved givens are permanently wired into foo's hash. The same scratch works split across files: drop class Show / given Show.nat into one file, add, then write the rest in a new scratch and resolution finds the givens from the namespace automatically.

---

How implicits/givens fit into Unison

Five principles are load-bearing:

1. Givens are sugar for ordinary parameters. After elaboration, a constraint is
   an ordinary positional argument. Runtime, codegen, ABT, and term hashing learn
   nothing new — the entire feature lives in the elaborator.

2. Resolution is baked into the term hash. A term that referenced Show Nat
   freezes the chosen dictionary's hash at typecheck time. Old terms never change
   instance. Unison gets something Scala and Haskell can't: implicits that are
   immune to "did adding this instance silently change my program?" — already-elaborated
   terms are pinned by content addressing.

3. Namespace = instance set. No orphan rules, no global registry. Two libraries
   that both define given Show.nat produce ambiguity at any call site that sees
   both, surfaced through the same machinery TDNR uses today.

4. Givenness is namespace metadata, not a term-level concept. Marking a
   definition given updates the namespace; term hashes are unchanged. The branch
   (causal) hash reflects the change. Aliasing, importing, forking work without
   rehashing terms.

5. Givens extend TDNR rather than replace it. TDNR resolves "which named
   definition fits this type"; given resolution adds "which value of this type
   exists, with chaining." Same elaborator pass, same ambiguity reporting.

Surface syntax

A class declaration generates getter accessors whose dictionary parameter is an => arrow (no setters, no modifiers):

class Show a = { show : a -> Text }
class Functor f = { fmap : forall a b. (a -> b) -> f a -> f b }

Plain records are still available with type Show a = Show (a -> Text); the difference is that class accessors carry the constraint implicitly, so callers write show x instead of Show.show dict x.

Declaring givens:

given Show.nat : Show Nat = Show Nat.toText

given Show.list : Show a => Show (List a) =
  Show (xs -> "[" ++ Text.join ", " (List.map Show.show xs) ++ "]")

given Functor.optional : Functor Optional = Functor Optional.map

The given keyword tags the binding so that, on add/update, namespace metadata is automatically updated — no follow-up mark.given needed (but the explicit command is still there if you want to flip an existing definition).

Consuming givens:

print : Show a => a ->{IO} ()
print x = printLine (Show.show x)

mapM : (Monad m, Traversable t) => (a ->{e} m b) -> t a ->{e} m (t b)

The summon builtin retrieves the unique resolvable dictionary at the surrounding context's expected type. Its declared type is forall a. a => a — the leading => makes the typechecker emit a constraint goal at every reference, which the resolver fills from lexical / ambient givens. At runtime summon is the identity function. Use it when you want to bind a dictionary explicitly:

sortReversed : Ord a => [a] -> [a]
sortReversed xs =
  given local : Ord a = Ord.flip (summon : Ord a)
  sort xs

summon is an ordinary term reference, so user code may shadow it.

The give keyword is the dual: give f demotes every leading => in f's declared type to ->, so the dictionaries become ordinary positional arguments at the call site. Use it for testing, mocking, or any time you want to bypass the resolver entirely:

combined : Show Nat => Monoid Nat => Nat -> Nat -> Text
combined a b = …

combined 3 4                        -- resolver picks Show.nat + Monoid.nat
give combined mockShow mulMonoid 3 4 -- both dicts supplied positionally

give has to be a keyword (not a builtin) because the type transformation can't be expressed as a regular polymorphic signature — the existing implicit-resolution rule would fire first on a builtin reference and the dictionary would be auto-filled before give could see it. Partial overrides (override one dict, let the resolver pick the rest) use the existing let given shadowing.

Resolution

For each constraint hole the elaborator searches visible givens whose conclusion
unifies with the goal type, recursively resolving each candidate's premises.
Ambiguity surfaces as the existing TDNR-style error. Cycles fail per-branch (the
candidate, not the whole search); a global depth limit (default 50) catches
runaway chains. Resolutions are memoized per top-level invocation, caching
successes and failures.

Specificity: A is strictly more specific than B iff some σ satisfies
σ(B's declared conclusion) = A's declared conclusion, with σ binding only B's
quantified variables. Local given beats outer given. Otherwise → ambiguity.

Coherence by content-addressing

The interplay between resolution and Unison's hashes is what makes this design
distinctive. A term containing a constraint hole elaborates to one containing
the chosen dictionary's hash. If the namespace later gains a second matching
given, the elaborated term is unchanged — its hash already commits to the
original. Only new terms see ambiguity.

This is stronger than Haskell's coherence (depends on global instance discovery
and orphan rules) and stronger than Scala's (can silently change on recompile).
Unison's content addressing makes coherence a non-issue for already-elaborated
code, by construction.

What's not in v1

• Functional dependencies / associated types
• Implicit conversions
• Default parameters
• deriving / macro derivation
• Kind-polymorphic givens (Unison's kind system has only Type, Ability, and
  arrow kinds)

What's in this PR

• Parser — => constraints, given declarations, let given,
  class declarations, @-positional explicit overrides.
• Namespace — ##Builtin.Given and ##Builtin.Class sentinels +
  MdValues plumbing on the term and type Stars respectively
  (Unison.Codebase.Givens / Unison.Codebase.Classes); UCM commands
  mark.given, unmark.given, givens; sharing-API round-trip;
  unison-merge conflict resolution for given-set diffs.
  given-declared bindings and class-declared types are auto-marked
  on add/update, and the slurp summary surfaces the class /
  given keyword in place of type / the plain term signature.
• Typechecker — Type.F extended with ImplicitArrow; lexical given
  environment threaded through every binder; constraint goals emitted at apply
  sites and at any Var/Ref use of a function with leading =>; =>I rule
  recognises the parser-injected leading lambda for a binding's implicit
  parameters and registers it as a lexical given for the body, so a polymorphic
  function's own =>-param resolves constraints raised inside its own body
  (this is what makes foldMap and polymorphic Show.list above work).
• Top-level givens promoted to the ambient pool — file-local given-tagged
  bindings are exposed to every goal in the file via the resolver's ambient
  pool, sidestepping minimize's reordering of independent SCCs (which could
  otherwise leave a sibling given invisible to an earlier user). Lexical
  registration is skipped for top-level givens so they don't tie with a
  function's own =>-parameter on the Lexical 0 scope tag.
• Speculative-pass info notes suppressed — annotateLetRecBindings's
  annotation-less redundancy pass and noteTopLevelType's redundancy-check
  synthesis both would leak ConstraintGoal notes with incomplete lexical
  scopes (because =>I never fires without the user's annotation). A
  discardInfoNotes combinator wraps both passes so only the
  official-typecheck constraint goals reach the resolver.
• summon builtin — summon : forall a. a => a, runtime identity. The
  => on its declared type drives implicit resolution through the normal
  machinery; the user writes (summon : T) (or relies on context) and gets
  back the unique resolvable given of type T.
• give keyword — give f is a prefix syntactic transformation that
  demotes every leading => in f's declared type to ->. Tagged with
  Ann.Lowered at parse time; the typechecker swaps peelLeadingImplicits
  for lowerLeadingImplicit at lowered references; GivenApply.rewriteApply
  pre-demotes the type — descending through any leading forall quantifiers
  first — before interleave sees it, so the decision queue stays aligned
  even for generalized signatures like forall a. C a => a -> a.
  Type.existentializeArrows no longer inserts an Effect row between
  adjacent =>s — implicit arrows carry no abilities. This was breaking
  the =>I checkWanted pattern on chained constraints like
  C1 => C2 => T.
• Resolver — full algorithm above, integrated as a post-pass on the
  TDNR fixed point; resolved decisions applied in the term as ordinary App
  nodes against dictionary hashes. Decisions are looked up by source location
  to keep multi-binding files coherent. decomposeGivenType strips the empty
  effect wrapper that generalization leaves around a constraint's conclusion,
  so a generalized polymorphic given unifies with the plain-shape goal at the
  call site.
• Errors — categorised NoGiven / Ambiguous / DepthExceeded /
  Cycle rendering. Resolution failures now surface through the file
  loader (previously the file silently failed to add).
• LSP — hover and goto-definition on synthesized implicit args;
  diagnostics and code actions for resolution failures.
• Pretty printer — => round-trips through view / edit /
  update. Elide-mode default: dictionary arguments inserted by the
  elaborator are not shown in surface output (so view foo matches
  what the user wrote); the corresponding leading \_implicit_*
  lambdas on the binding are also elided. The hash dependency is
  preserved — dependencies foo still lists the chosen given.
  view for class-tagged types emits the class keyword
  and renders the constructor with { field : type, ... } record syntax
  (driven by an IsClassRef predicate threaded through DeclPrinter,
  and hashClassFieldAccessors which reproduces the =>-bearing
  accessor hashes to recover field names from the namespace).
  view for given-tagged definitions emits the given keyword;
  view for terms that used give emits the give keyword with the
  user-supplied dictionary preserved (detected by walking each apply
  chain whose head has a =>-prefixed type and checking whether the
  dictionary argument is a namespace-tagged given or a local lexical
  given — anything else is treated as user-supplied via give and gets
  a sentinel Type.giveMarkerRef ascription that the surface printer
  recognises). The dependents-update path (prettyUnisonFile) consumes
  the file's classBindings so a class re-printed for re-typechecking
  keeps the class keyword and re-parses to the same hash.
• Tests — parser snapshot suite (60+ tests across => / given /
  summon / @); printer round-trip property tests; typechecker
  integration; full resolver test matrix including diamond dependencies
  and HKT; source-level end-to-end test pinning the parser → resolver
  wiring; UCM transcripts covering the update-semantics scenarios
  (updating a given changes the dependent's hash; breaking a given
  leaves old code valid; a new ambiguous given doesn't disturb old
  code).

stack build --fast clean. stack test --fast unison-parser-typechecker passes
(452/452).

Not ready yet

• given and give keyword migration — the prototype hard-breaks identifiers using
  the given and give names. The deprecation cycle is a release-engineering concern.
• unison-merge pipeline integration — the given-set conflict module
  is sidecar; wiring it into the merge engine is a follow-on.
• Resolver polish — cycle/metavar semantics, NearMiss substitution rendering,
  override-leaf parens diagnostic, partial-application handling, and more.

[Baccata]

The ambiguity errors need a bit of work : once several given instances of the same type are added to the codebase, they are referred to by hash instead of by name in the candidate list :

  I found multiple given candidates for Monoid Nat ; the choice is ambiguous.
  
      3 | main = do foldMap id [1, 2, 3, 4]
  
  
  Candidates:
    - #6lli3jv4to6spb4fh3fisr0olmoihuobg6i369s7drjj0d4emavdf8p6jlhacrf8mdotaak7lq97f3jp8dkdujbj0h5v3mnc4li7gq8
    - #eb24ogtms6mk9gldc3l1f37nrcc7l0lb3qicfjeoshmd8372huqd9m9bcoguc28pd4aad93hmj29vu9pffg7eqj71mg4modgddu88a8

Additionally, if I have a given instance in my codebase and an identical given instance in my scratch file, the elaborator seems to be unable to disambiguate the two :

-- this one was already added to the codebase
given Monoid.nat : Monoid Nat = Monoid (+) 0

main : 'Nat
main = do foldMap id [1, 2, 3, 4]

  I found multiple given candidates for Monoid Nat ; the choice is ambiguous.
  
      4 | main = do foldMap id [1, 2, 3, 4]
  
  
  Candidates:
  
    - ##Local.given.Monoid.nat
    - #eb24ogtms6mk9gldc3l1f37nrcc7l0lb3qicfjeoshmd8372huqd9m9bcoguc28pd4aad93hmj29vu9pffg7eqj71mg4modgddu88a8