MakeVarSat action can introduce shadowing

[brprice]

Code of conduct

• I've read the project's code of conduct, and agree to follow it.

Don't report security issues here

• I've read the project's security policy, and I do not believe this bug is a security issue.

Is there an existing issue?

• I've searched GitHub Issues, and I believe this is a new issue

What happened?

We currently try to ensure that "all" api calls do not introduce shadowing unless some shadowing already exists. However we have overlooked (at least) one case: the MakeVarSat action can splice (via unification) syntax between contexts.

There are some (rare) examples where this introduces shadowing. E.g. https://buildkite.com/hackworthltd/primer/builds/3976#018bf832-7799-48f6-9b83-2a31bbc9ae46 which had roughly the form:
starting with

foo : ? (∀z:*.?)
  = letrec z : ∀x:*.x
       = Λ_...
     in ?

we call MakeVarSat z in the term hole, generating the following

foo : ? (∀z:*.?)
  = letrec z : ∀x:*.x
       = Λ_...
     in z @(? (∀z:*.?))

This happens because we know the hole should have type ? (∀z:*.?), and z has type ∀x:*.x. We find some instantiation/application of z to unify these, and we see that ? (∀z:*.?) ∋ z @u if u = ? (∀z:*.?).

Note that we (i.e. the testsuite) consider the term binding letrec z and the type binding ∀z:* to shadow each other here. Slightly different examples would give two type variables shadowing.

What should have happened?

The action should have alpha-converted the unification solutions to not shadow.

Which package(s) or aspect(s) of the project are the source of the issue?

primer

Developers, please provide the output of the bug report script

The bug report script is running in a Nix shell.

System:
uname is:  Linux zephyrus 6.1.61 #1-NixOS SMP PREEMPT_DYNAMIC Thu Nov  2 08:35:33 UTC 2023 x86_64 GNU/Linux

Nix:
nix-build path is:  /run/current-system/sw/bin/nix-build
nix-build version is:  nix-build (Nix) 2.19.0pre20231103_aa85359
nix-command is enabled
flakes are enabled

direnv:
direnv is not in the PATH.

git:
git path is:  /run/current-system/sw/bin/git
git version is:  git version 2.40.1
git revision is:  6fe366c30be943b73c19c9ef8f12fd3ecd689ed1

make:
make path is:  /nix/store/s806iqg5vwsnp434i5whcn1rf605y9s6-gnumake-4.4.1/bin/make
make version is:  GNU Make 4.4.1
Built for x86_64-pc-linux-gnu
Copyright (C) 1988-2023 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <https://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Haskell:
ghc path is:  /nix/store/v7dl8207ll6g9sv92yjpav5w01c2ap0k-ghc-shell-for-packages-ghc-9.6.3-env/bin/ghc
ghc version is:  The Glorious Glasgow Haskell Compilation System, version 9.6.3
cabal path is:  /nix/store/by2phd5gqmdcqgx81prc906my8dw2bmk-cabal-install-exe-cabal-3.10.1.0/bin/cabal
cabal version is:  3.10.1.0

Sqitch:
sqitch path is:  /nix/store/aal1pllgrgjxigmmsk335z0q8599xzn1-sqitch-1.3.1/bin/sqitch
sqitch version is:  .sqitch-wrapped (App::Sqitch) v1.3.1
primer-sqitch path is:  /nix/store/v41yipjm8c0gizbjx9srn1jjqydrf6qj-primer-sqitch-1.0/bin/primer-sqitch

SQLite:
sqlite3 path is:  /nix/store/c7ywkkx5nb6g29236jbv3rdvv26i6kbn-sqlite-3.42.0-bin/bin/sqlite3
sqlite3 version is:  3.42.0 2023-05-16 12:36:15 831d0fb2836b71c9bc51067c49fee4b8f18047814f2ff22d817d25195cf350b0

Do you have a reproducer?

On commit 6fe366c, run cabal run primer-test -- --pattern '$NF ~ /available actions shadow/' --hedgehog-replay '96/808:bGlA Seed 15999972238796693072 1307829398512136357'

Any additional information?

Conceptually the bug is easy to fix, but I'm not sure how annoying it will be in practice.