typed holes (with subterms) for shrinking

A typed hole can have any type (it imposes no typing constraints on the context around it), and its subterms can have any type (the hole imposes no constraint on them).

This is the ultimate language construct to do type-preserving shrinking. When shrinking it is important to be able to remove subterms that do not participate to the error.

Holes with no subterms can be used to completely erase a term. Holes with subterms can be used to selectively erase parts of a term (for example, the application "t u" can be rewritten into the hole "...[t, u]", erasing only the application rule).

The MR also contains some independent improvements to the shrinking strategy; in particular convenient shrinking for products, which I hope to possibly upstream in QCheck directly.

client/test/TestMLRandom.ml

@@ -28,6 +28,7 @@ let rec size accu = function
   | ML.LetProd (_, t1, t2)
     -> size (size (accu + 1) t1) t2
   | ML.Tuple ts
+  | ML.Hole ts
     -> List.fold_left size (accu + 1) ts
   | ML.Match (t, brs)
     -> List.fold_left size_branch (size (accu + 1) t) brs
@@ -127,116 +128,166 @@ module Shrinker = struct
   module Shrink = QCheck.Shrink
   module Iter = QCheck.Iter
 
-  let rec fv x = function
+  let rec bv_pat = function
+    | ML.PVar y -> [y]
+    | ML.PWildcard | ML.PVariant (_, None) -> []
+    | ML.PAnnot (pat, _)
+    | ML.PVariant (_, Some pat) ->
+       bv_pat pat
+    | ML.PTuple ps ->
+       List.concat_map bv_pat ps
+
+  (* t[u/x] *)
+  let rec subst t x u =
+    match t with
     | ML.Var y ->
-       x = y
+      if x = y then u
+      else ML.Var y
     | ML.Abs (y, t) ->
-       if x = y then false
-       else fv x t
+      ML.Abs (y, subst_under [y] t x u)
     | ML.App (t1, t2) ->
-       fv x t1 || fv x t2
-    | ML.Let (y, t, u) ->
-       fv x t || (x <> y && fv x u)
+      ML.App (subst t1 x u, subst t2 x u)
+    | ML.Let (y, t1, t2) ->
+      ML.Let (y, subst t1 x u, subst_under [y] t2 x u)
     | ML.Tuple ts ->
-       List.exists (fv x) ts
-    | ML.LetProd (xs, t, u) ->
-       fv x t || (List.for_all ((<>) x) xs && fv x u)
-    | ML.Annot (t, _)
-    | ML.Variant (_, Some t) ->
-       fv x t
-    | ML.Variant (_, None) ->
-       false
+      ML.Tuple (List.map (fun t -> subst t x u) ts)
+    | ML.Hole ts ->
+      ML.Hole (List.map (fun t -> subst t x u) ts)
+    | ML.LetProd (ys, t1, t2) ->
+      ML.LetProd (ys, subst t1 x u, subst_under ys t2 x u)
+    | ML.Annot (t, ty) ->
+      ML.Annot (subst t x u, ty)
+    | ML.Variant (ty, t) ->
+      ML.Variant (ty, Option.map (fun t -> subst t x u) t)
     | ML.Match (t, brs) ->
-       fv x t || List.exists (fv_br x) brs
-
-  and fv_br x (pat, t) =
-    if bv_pat x pat then
-      false
-    else
-      fv x t
-
-  and bv_pat x = function
-    | PVar y ->
-       x = y
-    | PWildcard ->
-       false
-    | PAnnot (pat, _)
-    | PVariant (_, Some pat) ->
-       bv_pat x pat
-    | PVariant (_, None) ->
-       false
-    | PTuple ps ->
-       List.exists (bv_pat x) ps
-
-  let (let+) a f = Iter.map f a
-
-  let rec shrink_term gamma t = Iter.(
-    (match t, List.rev gamma with
-     | ML.Var _, _ ->
-        empty
-     | _, x0 :: _ ->
-        return (ML.Var x0)
-     | _, [] ->
+      ML.Match (subst t x u, List.map (fun br -> subst_branch br x u) brs)
+
+  (* (y.t)[u/x] *)
+  and subst_under ys t x u =
+    if List.mem x ys then t
+    else subst t x u
+
+  and subst_under_pat p t x u =
+    subst_under (bv_pat p) t x u
+
+  and subst_branch (p, t) x u =
+    (p, subst_under_pat p t x u)
+
+  let remove_variable t x =
+    subst t x (Hole [])
+  let remove_variables t xs =
+    List.fold_left remove_variable t xs
+
+  let rec shrink_term t = Iter.(
+    (* The Iter product is not suitable for shrinking:
+         (and+) (shrink a) (shrink b)
+       will try to shrink *both* a and b simultaneously,
+       but never try to shrink just one of them.
+
+       We shadow this unsuitable operator and use a "pointed product" (and++),
+       which tries to shrink a (with b constant) and then b (with a constant).
+
+       This corresponds to the behavior of Shrink.pair, but Shrink.pair works
+       on function types ('a -> 'a Iter.t), which is inconvenient
+       to write shrinkers directly -- no 'map' function. *)
+    let (and+) = () in ignore ((and+));
+    let (let++) (_a, it) f = Iter.map f it in
+    let (and++) (a, ita) (b, itb) =
+      (a, b),
+      Iter.append
+        (let+ a' = ita in (a', b))
+        (let+ b' = itb in (a, b'))
+    in
+    let subterms ts =
+      (* ...[t1, t2] is not always a desirable shrinking choice for a term
+         containing [t1, t2] as subterms, because it breaks the property that
+         the types of t1 and t2 appear in the resulting type, which is sometimes
+         important to reproduce typing bugs.
+         So we start with just (t1) and (t2) as shrinking choices,
+         even though they typically do not preserve typability. *)
+      of_list ts <+> return (ML.Hole ts) in
+    (match t with
+     | ML.Hole [] ->
         empty
+     | _ ->
+       return (ML.Hole [])
     ) <+> (
       match t with
       | ML.Var _ ->
          empty
 
+      | ML.Hole ts ->
+        (match ts with [t] -> return t | _ -> empty)
+        <+> (
+         let+ ts' = Shrink.list ~shrink:shrink_term ts
+         in ML.Hole ts'
+       )
+
       | ML.Abs (x, t) ->
-         let t' = shrink_term (x::gamma) t in
-         (if fv x t then empty else return t)
-         <+> (let+ t' = t' in ML.Abs (x, t'))
+         subterms [remove_variable t x]
+         <+> (
+           let+ t' = shrink_term t in
+           ML.Abs (x, t')
+         )
 
       | ML.App (t1, t2) ->
-         let t1' = shrink_term gamma t1 in
-         let t2' = shrink_term gamma t2 in
-         return t1
-         <+> t2'
-         <+> (let+ t1' = t1' and+ t2' = t2' in ML.App (t1',t2'))
+        subterms [t1; t2]
+        <+> (
+         let++ t1' = t1, shrink_term t1
+         and++ t2' = t2, shrink_term t2
+         in ML.App (t1',t2')
+       )
 
       | ML.Let (x, t, u) ->
-         let t' = shrink_term gamma t in
-         let u' = shrink_term (x::gamma) u in
-         return t
-         <+> (if fv x u then empty else return u)
-         <+> (let+ t' = t' and+ u' = u' in ML.Let (x, t', u'))
+        subterms [t; remove_variable u x]
+        <+> (
+         let++ t' = t, shrink_term t
+         and++ u' = u, shrink_term u
+         in ML.Let (x, t', u')
+       )
 
       | ML.LetProd (xs, t, u) ->
-         let t' = shrink_term gamma t in
-         let u' = shrink_term (xs@gamma) u in
-
-         return t
-         (* A more clever approach would be to inspect [t] to see if it is a
-            tuple and decrease the size of the tuple and the number of variables
-            in the let-binding, when the variable isn't free in the body.
-            For instance
-
-                 let (x, y, z) = (t1, t2, t3) in x z
-
-            can be shrunk into
-
-                 let (x, z) = (t1, t3) in x z
-          *)
-         <+> (let xs' = List.filter (fun x -> fv x u) xs in
-              if List.length xs == List.length xs' then
-                empty
-              else
-                match xs' with
-                | [] ->
-                   return u
-                | _ ->
-                   return (ML.LetProd (xs', t, u))
-             )
-         <+> (let+ t' = t' and+ u' = u' in ML.LetProd (xs, t', u'))
+        subterms [t; remove_variables u xs]
+        <+> (match t with
+          | ML.Hole _ ->
+            let+ xs' = Shrink.list_spine xs in
+            let u =
+              List.filter (fun x -> not (List.mem x xs')) xs
+              |> remove_variables u
+            in
+            if xs' = [] then u
+            else ML.LetProd (xs', t, u)
+          | _ -> empty
+        )
+        <+> (
+         let++ t' = t, shrink_term t
+         and++ u' = u, shrink_term u
+         in ML.LetProd (xs, t', u')
+       )
 
       | ML.Tuple ts ->
-         of_list ts
-         <+> let+ ts' = Shrink.list ~shrink:(shrink_term gamma) ts
-             in ML.Tuple ts'
+        subterms ts
+         <+> (
+           let+ ts' = Shrink.list ~shrink:shrink_term ts
+           in ML.Tuple ts'
+         )
+
+      | ML.Annot (t, _ty) ->
+        subterms [t]
+
+      | ML.Variant (lab, t) ->
+        subterms (Option.to_list t)
+        <+> (
+          match t with
+          | None -> empty
+          | Some t ->
+            let+ t' = shrink_term t
+            in ML.Variant (lab, Some t')
+        )
+
+      | ML.Match (_t, _branches) ->
+        failwith "unsupported"
 
-      | _ ->
-         assert false
     )
   )
 end
@@ -280,7 +331,7 @@ let () =
       let arb =
         QCheck.make
           ~print:MLPrinter.to_string
-          ~shrink:(Shrinker.shrink_term [])
+          ~shrink:Shrinker.shrink_term
           (term_gen (0, n))
       in
       let prop t =
@@ -297,7 +348,8 @@ let () =
         prop
   ) pairs in
   QCheck_runner.set_seed 0;
-  let _ = QCheck_runner.run_tests ~colors:true ~verbose:true tests in
+  let debug_shrink = None (* use (Some stdout) for a shrinking trace *) in
+  let _ = QCheck_runner.run_tests ~colors:true ~verbose:true ~debug_shrink tests in
   Printf.printf
     "In total, %d out of %d terms (%.1f%%) were considered well-typed.\n%!"
     !count_success !count_total