fix: EvalFull duplicated IDs and captures variables in BETA reduction

[brprice]

No description provided.

[brprice]

Maybe at some point in the future we can undo this change by adding lets in types. This may be necessary to implement #44

[georgefst]

Do we expect that adding such lets would be difficult? I suspect the symmetry would make interactive eval a lot easier to follow.

[georgefst]

Also, there's a missing closing parenthesis on line 369.

[brprice]

Do we expect that adding such lets would be difficult? I suspect the symmetry would make interactive eval a lot easier to follow.

I would expect it to be the same solution as supporting term-level let type in the typechecker #337. The issue is how to display types that may refer to the locally-bound name or its expansion.

[brprice]

The property tests we have "should have caught it eventually", but not in a reasonable timeframe. I would like to improve the generators (or add different tests) to improve the situation, but I don't have any good ideas on how to do this.

One thing I explored is to have a generator of BETA redexes, and test type preservation for that on its own. However, this rather targeted test still only picked up the bug roughly one test in 5000. For posterity, the code is pasted below

-- This test: generate random BETA redex in an environment with a typevar, check for type preservation
--
-- Bug was   (Λa. t : ∀b.T) S  ~~>  letType b=S in (letType a=S in t) : T
-- which can capture a 'b' in 'S' or 't'
hprop_tmp :: Property
hprop_tmp = withTests 1000 $
  withDiscards 2000 $ propertyWT [] $ do
      k <- forAllT genWTKind
      v <- forAllT genTyVarName
      (t, tyBeta) <- local (extendLocalCxtTy (v,k)) genBETA
      annotateShow t
      annotateShow tyBeta
      t' <- generateIDs $ LAM () v t
      let tyOrig = TForall () v k tyBeta
      _ <- checkTest tyOrig t'
      let chk e = do
            annotateShow e
            when (null [() | LetType{} <- universe e]) $ void $ checkTest tyOrig e
      let go i e | i >= 10 = pure ()
                 | otherwise = do
                   annotateShow i
                   e' <- evalFull mempty mempty 1 Chk e
                   case e' of
                     Left (TimedOut e'') -> chk e'' >> go (i +1) e''
                     Right e'' -> chk e''
      go 0 t'
  where
    genBETA = do
      k <- forAllT genWTKind
      a <- forAllT genTyVarName
      ty <- forAllT $ local (extendLocalCxtTy (a,k)) $ genWTType KType
      b <- forAllT $ genTyVarNameAvoiding ty
      ty' <- substTy a (TVar () b) ty
      t <- forAllT $ local (extendLocalCxtTy (b,k)) $ genChk ty'
      ty2 <- forAllT $ genWTType k
      tyRet <- substTy a ty2 ty
      pure (APP () (Ann () (LAM () b t) (TForall () a k ty)) ty2, tyRet)

[dhess]

Yikes, how did you find this one?

[dhess]

I confess that I don't understand the fix well enough to say anything particularly useful about it. I'm approving this so it can proceed, but also feel free to wait for @georgefst to have a look, if you prefer.

[brprice]

Yikes, how did you find this one?

Part of my search for shadowing and capture problems. I noticed when looking at the documented evaluation rule again.

[dhess]

I labeled this "Do not merge" as a note to myself until @georgefst has a chance to look at it upon his return.

[georgefst]

Do we expect that adding such lets would be difficult? I suspect the symmetry would make interactive eval a lot easier to follow.

[georgefst]

Also, there's a missing closing parenthesis on line 369.