fix #2053 by using Var.rawName to produce text for synthetic vars

[aryairani]

display <foo> stores results in the watch expression cache, which doesn't currently model the synthetic Vars that can come out of the runtime. This PR just flattens them down to Text.

[dolio]

So, the map example isn't actually correct, right?

If I recall, there's a problem where the numbers for these variables aren't actually displayed when used as terms for reasons I don't understand. Thus all pattern variables show up with rawName _pattern rather than _patternN. So, patterns will bind the correct variable, but then the occurrence in a term will reference the wrong variable.

I'm unclear on what the right fix is, though. On separate occasions, I've been told that this shouldn't be fixed, at least for some variables (like user variables), and should, probably for variables like these. I don't know exactly what is safe to change, and what expected consequences make it unsafe. But something needs to be done to prevent caching incorrect results.

[aryairani]

@dolio Bleh, thanks for catching that. I think it's a term-printer issue in this case? An inconsistency between how the numbers are rendered in pattern vars vs other vars, although I'm not certain because I didn't track down the spot (/cc @atacratic could you confirm or deny).

Let's sync up with @pchiusano next week and try to hash out what we'd need to change in order to begin to know exactly what's safe to change, and to know why whatever isn't wouldn't be, etc.

[dolio]

Okay, sounds good. I think there's some situation where it's discarding all the new numberings for fresh variables made up from user variables, because they "don't matter" or something. But I didn't understand why that was even safe at the time.

[pchiusano]

@aryairani @dolio okay yeah, this isn't quite the right fix, because the raw variable name may shadow or collide with another user-chosen name that's in the parent expression. In general, it's not safe to just rewrite a single variable using only local info like that, because of the possibility of collisions. You need to pass in something that is a closed term / type (no free vars) so the renaming of variables can be done in a way that avoids accidental capture.

If it's just a type signature you're tweaking, I think the correct fix will involve calling this function, passing it the full type:

unison/parser-typechecker/src/Unison/Typechecker/Context.hs

Lines 274 to 281 in 477371b

	-- The typechecker generates synthetic type variables as part of type inference.
	-- This function converts these synthetic type variables to regular named type
	-- variables guaranteed to not collide with any other type variables.
	--
	-- It also attempts to pick "nice" type variable names, based on what sort of
	-- synthetic type variable it is and what type variable names are not already
	-- being used.
	removeSyntheticTypeVars :: Var v => Type.Type v loc -> Type.Type v loc

It will pick nice type variable names and avoid variable capture.

If you have a term with embedded annotations, then you might have to do something fancier to avoid capturing type variables from an outer scope. Hmm, thinking through this, I'm not sure it's possible for a type signature to refer to synthetic type variables in an outer scope. By design, there's no syntax for synthetic type variables, so the user can't write them in an explicit type signature. And the only way to capture a type variable from an outer scope is with an explicit type signature. So it seems that just recursively calling removeSyntheticTypeVars on any embedded type annotations in a term might be fine.

If it were necessary to do something fancier to deal with scoped type variable capture inside of terms, these functions do that properly and you could probably take inspiration from them and I'd be happy to pair.

unison/unison-core/src/Unison/Term.hs

Line 295 in 98f2ed3

freeTypeVars :: Ord vt => Term' vt v a -> Set vt

unison/unison-core/src/Unison/Term.hs

Lines 311 to 314 in 98f2ed3

	substTypeVars :: (Ord v, Var vt)
	=> [(vt, Type vt b)]
	-> Term' vt v a
	-> Term' vt v a

[aryairani]

This function is just about converting a single symbol from one format to another, and this PR is just about fixing a crash in it.

What you're saying sounds to me like there's a bigger problem that's unrelated to this function or this PR. We get the same bad pretty-term even with --old-codebase, which doesn't call this code.

So I think we should merge this and open a ticket for the thing I don't yet understand, and maybe @dolio could take point on? 🙏

WDYT?

[aryairani]

I could back out or move the transcript, given that the output is wrong, but it's not related to this PR; the point was that it produces output at all now instead of crashing, and there could also be existing transcripts that are wrong for the same reason.

[pchiusano]

@aryairani yeah, I'm okay with merging as is, just to avoid the crash, even though it's not correct, as long you create a separate ticket to track the proper fix.

It will only come up if someone picks one of those weird blackboard symbols for a type signature, which I think should be pretty rare.

[aryairani]

@pchiusano Our example case wasn't due to blackboard symbols, but due to pretty-printing a value that is a function that does pattern matching:

.> view List.map

  base.List.map : (a ->{𝕖} b) -> [a] ->{𝕖} [b]
  base.List.map f a =
    go i as acc =
      match List.at i as with
        None   -> acc
        Some a ->
          use Nat +
          go (i + 1) as (acc :+ f a)
    go 0 a []

.> display List.map

  go f i as acc =
    _pattern = List.at i as
    match _pattern with
      None           -> acc
      Some _pattern1 ->
        use Nat +
        go f (i + 1) as (acc :+ f _pattern)
  f a -> go f 0 a []

[hojberg]

@aryairani @dolio @pchiusano did this also fix #2144 ? (seems similar to #2053)

[aryairani]

@aryairani @dolio @pchiusano did this also fix #2144 ? (seems similar to #2053)

@hojberg #2144 reports two bugs, only the second of which was fixed by this.