Fix a shadowing bug in generating recursive types. (IntersectMBO#3934)

* Remove a workaround for a fixed bug

* Insert more pedantic checks

* Fix a bug relating to reusing a variable name in two binders

This turns out to be benign so long as you rename, but we might as well
not introduce extra pointless shadowing if we don't have to.

* Rename before typechecking when doing paranoid checks

* Fix tests with uniques in

Author: michaelpj

plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Type.hs

@@ -744,10 +744,12 @@ makeRecursiveType1
 makeRecursiveType1 ann dataName argVar patBody1 = do
     let varName = _tyVarDeclName argVar
         varKind = _tyVarDeclKind argVar
+    varName' <- freshenTyName varName
+    let
         recKind = KindArrow ann varKind $ Type ann
         pat1 = TyLam ann dataName recKind $ TyLam ann varName varKind patBody1
         -- recType = \(v :: k) -> ifix (\(dataName :: k -> *) (v :: k) -> patBody1) v
-        recType = TyLam ann varName varKind . TyIFix ann pat1 $ TyVar ann varName
+        recType = TyLam ann varName' varKind . TyIFix ann pat1 $ TyVar ann varName'
         wrap args = case args of
             [arg] -> iWrap ann pat1 arg
             _     -> throw . IndicesLengthsMismatchException 1 (length args) $ dataName

plutus-core/plutus-ir/src/PlutusIR/Compiler.hs

@@ -141,7 +141,8 @@ typeCheckTerm t = do
 check :: Compiling m e uni fun b => Term TyName Name uni fun (Provenance b) -> m ()
 check arg = do
     shouldCheck <- view (ccOpts . coPedantic)
-    if shouldCheck then typeCheckTerm arg else pure ()
+    -- the typechecker requires global uniqueness, so rename here
+    if shouldCheck then typeCheckTerm =<< PLC.rename arg else pure ()
 
 -- | The 1st half of the PIR compiler pipeline up to floating/merging the lets.
 -- We stop momentarily here to give a chance to the tx-plugin
@@ -185,25 +186,21 @@ compileReadableToPlc =
     >=> through check
     >=> (<$ logVerbose "  !!! compileLets RecTerms")
     >=> Let.compileLets Let.RecTerms
-    -- TODO: add 'check' steps from here on. Can't do this since we seem to generate a wrong type
-    -- somewhere in the recursive binding compilation step
     >=> through check
     -- We introduce some non-recursive let bindings while eliminating recursive let-bindings, so we
     -- can eliminate any of them which are unused here.
-    >=> (<$ logVerbose "  !!! rename")
-    >=> PLC.rename
-    >=> through check
-    -- NOTE: There was a bug in renamer handling non-rec terms, so we need to
-    -- rename again.
-    -- https://jira.iohk.io/browse/SCP-2156
     >=> (<$ logVerbose "  !!! removeDeadBindings")
     >=> DeadCode.removeDeadBindings
+    >=> through check
     >=> (<$ logVerbose "  !!! simplifyTerm")
     >=> simplifyTerm
+    >=> through check
     >=> (<$ logVerbose "  !!! compileLets Types")
     >=> Let.compileLets Let.Types
+    >=> through check
     >=> (<$ logVerbose "  !!! compileLets NonRecTerms")
     >=> Let.compileLets Let.NonRecTerms
+    >=> through check
     >=> (<$ logVerbose "  !!! lowerTerm")
     >=> lowerTerm
 

plutus-core/plutus-ir/test/datatypes/listMatchEval.golden

@@ -1 +1 @@
-(delay (lam x_138 x_138))
+(delay (lam x_85 x_85))

plutus-core/plutus-ir/test/recursion/even3Eval.golden

@@ -1 +1 @@
-(delay (lam case_True_365 (lam case_False_366 case_False_366)))
+(delay (lam case_True_228 (lam case_False_229 case_False_229)))

plutus-core/plutus-ir/test/types/listMatch.golden

@@ -1 +1 @@
-(fun (con integer) (all a_48 (type) (fun a_48 a_48)))
+(fun (con integer) (all a_49 (type) (fun a_49 a_49)))

plutus-core/plutus-ir/test/types/mutuallyRecursiveTypes.golden

@@ -1 +1 @@
-[ Forest_11 (all a_42 (type) (fun a_42 a_42)) ]
+[ Forest_11 (all a_44 (type) (fun a_44 a_44)) ]