EvalFull does not (quite) have type preservation

brprice commented 2 years ago

What happened?

I have a program which is well-typed. I ran one step of EvalFull on it and received a program that is ill-typed. (Actually, this was seen in CI: https://buildkite.com/hackworthltd/primer/builds/2263#01842afa-92dd-499e-aa77-60f44dcba2c4, but I have got a better reproducer)

Note that I know what the underlying problem is and have a few ideas (and some code) to fix it -- I have not made a pr as I'd like to discuss which approach to take.

What did you expect to happen?

Evaluating a well-typed program should result in a well-typed program.

How can we reproduce it?

This exists on main 1982c56ce4ac50107386a8ddcd76309fac241cac and I suspect has existed essentially forever. Run the following code which constructs an expression, checks it is well-typed, does one step of evaluation and shows the result is ill-typed. It also pretty prints the two expressions. (Note that one could rename to unit_... and it would be picked up by the testsuite; however because of the pretty printing it does not make a good testsuite addition as-is.)

ci2263_bug :: IO ()
ci2263_bug = evalTestM 0 $ do
  t <- case_ ((con cJust `aPP` tEmptyHole `app` con cFalse) `ann` (tcon tMaybe `tapp` tcon tNat))
    [branch cNothing [] emptyHole
    ,branch cJust [("x",Nothing)] $ con cSucc `app` lvar "x"]
  let tds = foldMap moduleTypesQualified testModules
  let globs = foldMap moduleDefsQualified testModules
  ((_steps, s), logs) <- runPureLogT $ evalFullStepCount tds globs 1 Syn t
  let s' = case s of
        Left (TimedOut e) -> e
        Right e -> e
  pure $ do
      putStrLn @Text "Before"
      prettyPrintExpr compact t
      expectTypedWithPrims $ pure t `ann` tEmptyHole
      putStrLn @Text "After"
      prettyPrintExpr compact s'
      assertNoSevereLogs @EvalFullLog logs
      expectTypedWithPrims $ pure s' `ann` tEmptyHole

Note that it throws a hunit exception (which is somewhat hard to read) because of InconsistentTypes, i.e. TC failed, in the last line.

How severe is the bug?

It is fairly rare, and only effects evaluation.

What's your environment?

NixOS, ghc from nix develop on the commit listed above.

Any additional information?

For the particular example above, we have the well-typed initial term case (Just @? False : Maybe Nat) of {Nothing -> ? ; Just x -> Succ x} evaluating in one step to the ill-typed let x = (False : Nat) in Succ xfix: type preservation for evaluating case redex

This happens because evaluating a case-of-known-constructor results in the RHS of the appropriate branch wrapped in some let bindings for each argument to the constructor. These bindings are annotated with their type. Unfortunately, we have two choices for where to get this type from, and they do not agree!

The constructor Just @? False (plus the definition of Maybe) implies that we should bind x = False : ?
The type annotation Maybe Nat (plus the definition of Maybe) implies that the argument to the constructor must be of type Nat, and thus we bind x = ... : Nat Note that without type holes (which essentially act as a type-cast here), we would know that these two pieces of information would agree. Indeed, we know that they agree up to holes. Note also that if we considered constructors as checkable only then we would only have one source of information and the problem would not exist (the analogous input scrutinee Just False : Maybe Nat would also be ill-typed)

Note that in we purposefully choose the second option (from the type annotation), since the branch's rhs expects x ∈ Nat, since typechecking only cares about the type of the scrutinee.

I see three options on how to fix this.

Firstly, consider our synthesisable constructors as shorthand Just @? False means Just False : Maybe ?, or synthesisable-Just means (Λa.λx. JUST x) : ∀a.a -> Maybe a (where this JUST is the "checkable constructor"). This would imply we should treat it the same as case ((JUST False : Maybe ?) : Maybe Nat) of {Nothing -> ? ; Just x -> Succ x} which is a stuck term -- we don't have the right form for a case reduction, and we cannot remove the Maybe ? annotation since it is not "concrete" (no type holes or variables). In the implementation, we would simply refuse to do a case reduction if any of the type arguments to the constructor had holes in (and maybe variables -- whether this is important needs a bit of thought)

Secondly, let's assume our calculus has the nice meta-theoretical property of "making judgement inputs more holey will make the outputs more holey, but still be well-typed". Then we can just take the "meet" of the two choices above (i.e. replace the minimal subterms with holes such that they agree). The correctness of this relies on case expressions being checkable. A sketch of a justification is:

consider a subexpression case e of C x -> t such that typechecking the program requires S ∋ case e of C x -> t and thus, assuming e ∈ T A, we also require x : B[A] |- S ∋ t (for some B as dictated by the definition of T).
for well-typedness, all we require of the reduct is that it inhabits the type S (although to preserve semantics we would need more!), since case is in the checkable fragment
the reduct will be of the form let x = ... : X in t, and for this to inhabit S we need x : X |- S ∋ t. Thus any X which is "more hole-y" than B[A] suffices
this x will be some argument to an explicit constructor: e = C @A' r : T A will lead to let x = r : B[...] in t which will further require that B[...] ∋ r, thus we will need X more hole-y than B[A'] (note the difference between A and A' here!)

However, this nice metatheoretical property does not (quite) hold! (I'd argue that this is not the correct state of affairs). This is for two small reasons. Making the inputs more hole-y may:

change a higher-kinded forall ∀a:(k1 -> k2).... into a type hole. Currently typeholes can only act as foralls quantified over KType, so this would break judgements such as t : ∀a:(* -> *). * |- * ∋ t Maybe being replaced by t : ? |- * ∋ t Maybe
change the type of a case scrutinee into ?. The judgement for case expressions is very strict about what the branches are. In particular, if the scrutinee has type ?, then there must be no branches whatsoever. However, there may well be branches since the previous type of the scrutinee may have been Nat (etc).

This would be fairly straightforward to fix (although some thought about interaction/Actions for the second problem is needed). We would need

756
to relax the typechecker wrt what branches are allowed in hole-typed case expressions
we will also need to relax the notion of "consistent type" (i.e. "same up to hole") to include comparing the kind-annotation on foralls up to holes also (at least, in the strong case where we want the metaproperty to hold for making such kinds hole-y-er).

This is investigated in my branch https://github.com/hackworthltd/primer/tree/brprice/holeyer-type-pres

Thirdly, in a similar vein to the first option, we could annotate the let-bound variables twice: case (Just @? False : Maybe Nat) of {Nothing -> ? ; Just x -> Succ x} evaluates in one step to let x = (False : ? : Nat) in Succ x which is type-correct.

However, this could lead to let x = (False : ? : ?) if the annotation and constructor both had holes, which would annoyingly not reduce (we only elide annotations if they are non-holey) -- we probably want to only put one copy of identical annotations on)

(I imagine that we could consider generalising this by treating ctors as shorthand for annotated things, and having a rule about reducing something of the form case C xs : T As : T Bs : ... : T Zs of C ys -> t to let ys=xs:S[As]:S[Bs]:...:S[Zs] in t, and similarly for other beta rules. I have no idea if this would be nice UX though!)

This is investigated in my branch https://github.com/hackworthltd/primer/tree/brprice/case-ty-pres-double-ann, and in #769

georgefst commented 2 years ago

I was surprised to see that Just @? False : Maybe Nat actually typechecks. It doesn't in Haskell for example, and I hadn't previously considered how our type holes are different.

Anyway, option 2 sounds like the more elegant solution.

dhess commented 2 years ago

If I understand it correctly (I'm a bit fuzzy on some of the type theory in option 2), this bit makes me nervous about option 2:

to relax the typechecker wrt what branches are allowed in hole-typed case expressions

Also IIUC, I think I'm ok with refusing to do case reductions per solution 1.

brprice commented 2 years ago

If I understand it correctly (I'm a bit fuzzy on some of the type theory in option 2), this bit makes me nervous about option 2:

to relax the typechecker wrt what branches are allowed in hole-typed case expressions

Huh, I thought you had previously argued in favor of being more lenient here.

dhess commented 2 years ago

I think what I've previously argued is that we should respect the student's work and not arbitrarily delete expressions that they've written (e.g., per current discussion, when the branches of a match with change due to a change in the type of the scrutinee).

I don't think I argued that we specifically need to preserve those no-longer-type-correct expressions by relaxing the typechecker to accept nonsensical match with branches. (It's been awhile, perhaps I'm wrong.)

Most recently, I advocated for using a modules-as-records system to solve this: https://docs.craft.do/editor/d/8b43f204-aeeb-b8ce-45cc-73a653745299/C5C2348A-1D95-4CDE-9568-070FCFB744A5/b/96397B2B-06B3-4EDB-86F0-698F165DCA6F#B6B72B14-02ED-4DA8-ACA3-358CF63B343A

brprice commented 1 year ago

Note: I have edited in an option 3, about double-annotating let bindings

brprice commented 1 year ago

We discussed this in our 2022-11-08 developer meeting, and came up with a few questions:

Can this arise "naturally" from evaluating a "sensible" input program?

By this we mean, something more likely in practice than case Just @? False : Maybe Nat of ... as an input.

One somewhat-sensible way is having a top-level-definition doubleOrZero : Maybe Nat -> Nat = λx.case x of Just y -> 2*y; Nothing -> 0, and evaluating doubleOrZero (Just @? True). This could arise from the construction sequence ?, Just @? ?, Just @? True, ? (Just @? True), doubleOrZero (Just @? True). However, note that this is not particularly satisfying for two reasons:

if one did the doubleOrZero ? construction first and then filled in that hole with a "refined constructor" one would obtain doubleOrZero (Just @Nat ?)
if we offered a "fill in obvious type holes" facility, then writing Just @? True could automatically turn into Just @Bool True Unfortunately I don't currently have a more satisfying "natural" example.

What are some concrete evaluation traces showing the issue and each proposed solution?

Consider the above example. Regardless of the case-of-known-constructor reduction rule we get the sequence doubleOrZero (Just @? True) (λx.case x of Just y -> 2*y; Nothing -> 0 : Maybe Nat -> Nat) (Just @? True) (let x = Just @? True : Maybe Nat in case x of Just y -> 2*y; Nothing -> 0) : Nat (case Just @? True : Maybe Nat of Just y -> 2*y; Nothing -> 0) : Nat Let's assume we are in a checkable context so I can elide the outer annotation: case Just @? True : Maybe Nat of Just y -> 2*y; Nothing -> 0 I shall refer to this last expression as EXPR

Now the choice of rule matters.

Under the status quo we then reduce to let y = True : Nat in 2*y 2*(True : Nat) 2*True where this last step is because we can elide any concrete annotation in a checkable position (and * is a function, so its arguments are checkable: indeed, we know its arguments must be of type Nat). Clearly this output is nonsense, and the problem arose in the very first line where we had True : Nat.

Under option 1 "synthesisable constructors are shorthand for annotated checkable ones" we would have that EXPR means case (JUST True : Maybe ?) : Maybe Nat of Just y -> 2*y; Nothing -> 0 which is a stuck term, since this is not case-of-known-constructor, and the inner annotation cannot be elided since it has a hole (and thus may, indeed does, act as a type-changing cast), and the outer annotation cannot be elided as it is in synthesisable position.

Under option 2 "take the 'meet'" we would get EXPR is case Just @? True : Maybe Nat of Just y -> 2*y; Nothing -> 0 which would reduce to let y = True : ? in 2*y since the 'meet' of ? and Nat is ?. It would further reduce as 2*(True : ?) and get stuck.

Under option 3 "annotate twice" we would get EXPR is case Just @? True : Maybe Nat of Just y -> 2*y; Nothing -> 0 which would reduce to let y = (True : ?) : Nat in 2*y which reduces to 2*((True : ?) : Nat) 2*(True : ?) and gets stuck.

Note that options 2 and 3 happen to give the same result here, but this is not the case in general. We could have something of the form case (C @? @B _ : T A ?) of ... which would (respectively) give annotations _ : T ? ? or _ : T ? B : T A ?. (This gives the orthogonal idea that possibly we could/should have an "upsilon" rule that coalesces adjacent annotations by taking the "meet". If we did not have type holes this would be redundant since the inner one would be elidable, but that is not the case with holes! See https://github.com/hackworthltd/primer/issues/12#issuecomment-1307261788)

dhess commented 1 year ago

For the record, we decided to implement option 3 for now as we expect this is not super-likely to occur, and therefore has low priority (and option 3 has more or less already been implemented in a waiting branch).

However, we'll keep this open until we are ready to tackle two related issues: should holes be reducible, or should they get stuck? and what to do about student-defined patterns, as that feature will also open the door to arbitrary-ish case branches à la option 2 here.

brprice commented 1 year ago

The immediate problem was fixed with #769 (implements "option 3"), and this issue was left open for further/related discussion. Since then, we have changed constructors to be checkable and not store their indices, completely side-stepping the immediate problems in this issue. Since we have diverged so much from the initial report, I am closing this.

Feel free to open new issues to discuss related topics.

hackworthltd / primer