Improve 'raise' to introduce let bindings for newly out-of-scope vars

[brprice]

This is a placeholder for now, I will come back and fill this in later.

If we want to do this generically for copy/paste, we may want to use letType to deal with typevars. This would need us to fix #5.
However, we may not want to do this, for consistency with the type level copy/paste which has no lets. It is also a bit pointless as it wouldn't be exposed to the user of raise, as you cannot hit this situation with that tool. (Well, you could do ? : ∀a . List a, and try to lift the List a to get ? : List ?. We could instead give lettype a = ? in ? : List a, by introducing a lettype outside the annotation, but I suspect this is more confusing than it is worth!) Edit: scrap that, you could have Λa . (? : List a), and raise this to get ? : List ?.

We will want to consider how to make this non-annoying when lifting the body of a lambda etc (or worse, a let!). Going from (λx.t) to let x = ? in t doesn't seem all that useful for raise!

Description

This is a feature request.

<Include a brief description here.>

Dependencies

<Link to other GitHub Issues or PRs that must be completed before work can begin on this feature.>

Spec

<Describe what the feature will do, from a high-level perspective.>

Implementation details

<If there are any particularly tricky implementation bits that are worth discussing or you haven't quite figured out yet, describe the details here.>

Not in spec

<Describe any features that your implementation is explicitly avoiding, that a reasonable person might think should be in spec. For example, if you're adding a new action that operates on variables, but it only works with term variables and not type variables, you might want to mention it here so that the scope of the feature is clear.>

Discussion

<If there's a GitHub Discussions topic where this feature has been/is being discussed, link it here.>

Future work

<Describe ideas or additional features that might be useful once this feature has been implemented. This is a good place to link to other GitHub Issues or PRs that track this future work.>

[brprice]

One testcase that may be useful if we want to use letType could be this diff (still commented out) [I am recording this here so I don't lose it when I tidy up my branch for implementing basic duplicate)

commit dfe633411a31d26a4e0e62a2b619f0c37ce16138 (HEAD -> brprice/duplicate, tag: duplicate-saussage-including-notes-to-put-in-issue)
Author: Ben Price <[email protected]>
Date:   Thu Jul 1 14:57:58 2021 +0100

    upgrade test of let-intro when paste to also care about type lets; can't implement until can TC typelet

diff --git a/backend/core/test/ProgActionTest.hs b/backend/core/test/ProgActionTest.hs
index 38a3c384..13d0453d 100644
--- a/backend/core/test/ProgActionTest.hs
+++ b/backend/core/test/ProgActionTest.hs
@@ -267,22 +267,22 @@ prop_raise = withTests 1 $ property $ do
       in
        clearIDs (progDefs r) === clearIDs (progDefs tcpExpected)
 
--- ∀a. List a -> Maybe a
--- /\a . λ x . case x of Nil -> ? ; Cons y ys -> Just @a y
+-- ∀a. List a -> ∀b. b -> Pair a b
+-- /\a . λ x . case x of Nil -> ? ; Cons y ys -> /\@b z -> Pair @a @b y z
 -- copy the Just @a y into the hole to get
--- /\a . λ x . case x of Nil -> let y = ? : a in Just @a y ; Cons y ys -> Just @a y
+-- /\a . λ x . case x of Nil -> lettype b = ? in let y = ? : a in Pair @a @b y z ; Cons y ys -> /\@b z -> Pair @a @b y z
 prop_copy_paste_expr_1 :: Property
 prop_copy_paste_expr_1 = withTests 1 $ property $ do
   let ((pInitial,defID,srcID,pExpected),maxID) = create $ do
         defID' <- fresh
-        ty <- tforall "a" KType $ (tcon "List" `tapp` tvar "a") `tfun` (tcon "Maybe" `tapp` tvar "a")
-        let toCopy' = con "Just" `aPP` tvar "a" `app` var "y" -- want different IDs for the two occurences in expected
+        ty <- tforall "a" KType $ (tcon "List" `tapp` tvar "a") `tfun` (tforall "b" KType $ tvar "b" `tfun`(tcon "Pair" `tapp` tvar "a" `tapp` tvar "b"))
+        let toCopy' = con "MakePair" `aPP` tvar "a" `aPP` tvar "b" `app` var "y" `app` var "z" -- want different IDs for the two occurences in expected
         toCopy <- toCopy'
         let skel r = lAM "a" $ lam "x" $ case_ (var "x")
                  [branch "Nil" [] r
-                 ,branch "Cons" [("y",Nothing),("ys",Nothing)] $ pure toCopy]
-        expectPasted <- con "Just" `aPP` tvar "a" `app` emptyHole
-        --expectPasted <- let_ "y" (emptyHole `ann` tvar "a") toCopy' -- TODO: reinstate when actually produce bindings
+                 ,branch "Cons" [("y",Nothing),("ys",Nothing)] $ lAM "b" $ lam "z" $ pure toCopy]
+        expectPasted <- con "MakePair" `aPP` tvar "a" `aPP` tEmptyHole `app` emptyHole `app` emptyHole
+        --expectPasted <- letType "b" tEmptyHole $ let_ "y" (emptyHole `ann` tvar "a") $ let_ "z" (emptyHole `ann` tvar "b") toCopy' -- TODO: reinstate when actually produce bindings
         defInitial <- Def defID' "main" <$> skel emptyHole <*> pure ty
         expected <- Def defID' "main" <$> skel (pure expectPasted) <*> pure ty
         pure $ (newProg {progDefs = Map.fromList [(defID', defInitial)]}