unison/unison-src/transcripts/fix1578.md

This transcript shows how suffix-based name resolution works when definitions in the file share a suffix with definitions already in the codebase.

Setup

scratch/main> builtins.merge

As setup, we'll add a data type Day and a definition foo.bar : Nat.

unique type Day = Sun | Mon | Tue | Wed | Thu | Fri | Sat

foo.bar : Nat
foo.bar = 23

scratch/main> add

Suffix-based name resolution prefers to use names locally defined in the current file, then checks for matches in the codebase. Here are the precise rules, which will be explained below with examples:

• If a symbol, s, is a suffix of exactly one definition d in the file, then s refers to d.
• Otherwise, if s is a suffix of exactly one definition d in the codebase, then s refers to d.
• Otherwise, if s is a suffix of multiple definitions in the file or the codebase, then (at least for terms) type-directed name resolution will be attempted to figure out which definition s refers to.

Example 1: local file term definitions shadow codebase term definitions

This should typecheck, using the file's bar : Text rather than the codebase foo.bar : Nat:

use Text ++

bar : Text
bar = "hello"

baz = bar ++ ", world!"

Example 2: any locally unique term suffix shadows codebase term definitions

This should also typecheck, using the file's oog.bar. This shows you can refer to a definition in the file by any suffix that is unique to definitions in the file (even if that suffix may match other definitions in the codebase). See example 4 below for overriding this behavior.

use Text ++

oog.bar = "hello"

baz = bar ++ ", world!"

This subtle test establishes that we aren't using type-directed name resolution (TDNR) for the local term references in the file. If this were using TDNR, it would fail with an ambiguity as there's nothing that pins down the expected type of bar here:

use Text ++

oog.bar = "hello"

baz = (bar, 42)

This subtle test establishes that locally introduced variables (within a function, say) correctly shadow definitions introduced at the file top level:

use Text ++

oog.bar = "hello"

baz : [Int] -> ([Int], Nat)
baz bar = (bar, 42) -- here, `bar` refers to the parameter

Example 3: Local type and constructor definitions shadow codebase definitions

This should also typecheck, using the local Sun, and not Day.Sun which exists in the codebase, and the local Day, not the codebase Day.

structural type Zoot = Zonk | Sun

structural type Day = Day Int

use Zoot Zonk

flip : Zoot -> Zoot
flip = cases
  Sun -> Zonk
  Zonk -> Sun

day1 : Day
day1 = Day +1

Example 4: Refering to codebase definitions via a unique suffix

Even though local definitions are preferred, you can refer to definitions in the codebase via any unique suffix that doesn't also exist in the file.

structural type Zoot = Zonk | Sun

use Zoot Zonk

blah = cases
  Day.Sun -> Day.Tue
  day -> day

blah2 =
  -- imports work too if you get tired of typing Day.Sun over and over
  use Day Sun
  cases Sun -> Wed
        day -> day