Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 1 commit into from
Jun 29, 2021
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions parser-typechecker/src/Unison/Codebase/SqliteCodebase/Conversions.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -242,8 +242,7 @@ symbol2to1 :: V2.Symbol -> V1.Symbol
symbol2to1 (V2.Symbol i t) = V1.Symbol i (Var.User t)

symbol1to2 :: V1.Symbol -> V2.Symbol
symbol1to2 (V1.Symbol i (Var.User t)) = V2.Symbol i t
symbol1to2 x = error $ "unimplemented: symbol1to2 " ++ show x
symbol1to2 (V1.Symbol i varType) = V2.Symbol i (Var.rawName varType)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

@aryairani aryairani Jun 28, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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 []


shortHashSuffix1to2 :: Text -> V1.Reference.Pos
shortHashSuffix1to2 =
Expand Down
7 changes: 7 additions & 0 deletions unison-src/transcripts/fix2053.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
```ucm:hide
.> builtins.mergeio
```

```ucm
.> display List.map
```
13 changes: 13 additions & 0 deletions unison-src/transcripts/fix2053.output.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
```ucm
.> 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 []

```