Hiding extra information in the IDE, sorting trees.

crates/argus/src/ext.rs

@@ -43,6 +43,8 @@ pub trait PredicateExt {
   fn is_rhs_lang_item(&self, tcx: &TyCtxt) -> bool;
 
   fn is_trait_pred_rhs(&self, def_id: DefId) -> bool;
+
+  fn is_lhs_ty_var(&self) -> bool;
 }
 
 impl PredicateExt for Predicate<'_> {
@@ -66,6 +68,18 @@ impl PredicateExt for Predicate<'_> {
       trait_predicate.def_id() == def_id
     })
   }
+
+  fn is_lhs_ty_var(&self) -> bool {
+    match self.kind().skip_binder() {
+      ty::PredicateKind::Clause(ty::ClauseKind::Trait(trait_predicate)) => {
+        trait_predicate.self_ty().is_ty_var()
+      }
+      ty::PredicateKind::Clause(ty::ClauseKind::TypeOutlives(
+        ty::OutlivesPredicate(ty, _),
+      )) => ty.is_ty_var(),
+      _ => false,
+    }
+  }
 }
 
 pub trait StableHash<'__ctx, 'tcx>:

crates/argus/src/proof_tree/mod.rs

@@ -16,8 +16,8 @@ pub use topology::*;
 use ts_rs::TS;
 
 use crate::{
-  ext::InferCtxtExt,
-  serialize::{serialize_to_value, ty::Goal__PredicateDef},
+  ext::{InferCtxtExt, PredicateExt},
+  serialize::{safe::GoalPredicateDef, serialize_to_value},
   types::{
     intermediate::{EvaluationResult, EvaluationResultDef},
     ImplHeader, ObligationNecessity,
@@ -63,10 +63,13 @@ pub struct Goal {
   #[cfg_attr(feature = "testing", ts(type = "EvaluationResult"))]
   result: EvaluationResult,
 
-  // TODO: remove this is only for debugging
-  debug_comparison: String,
   necessity: ObligationNecessity,
   num_vars: usize,
+  is_lhs_ty_var: bool,
+
+  #[cfg(debug_assertions)]
+  #[cfg_attr(feature = "testing", ts(type = "string | undefined"))]
+  debug_comparison: String,
 }
 
 #[derive(Serialize, Clone, Debug, PartialEq, Eq)]
@@ -115,24 +118,21 @@ impl Goal {
     goal: &solve::Goal<'tcx, ty::Predicate<'tcx>>,
     result: EvaluationResult,
   ) -> Self {
-    #[derive(Serialize)]
-    struct Wrapper<'a, 'tcx: 'a>(
-      #[serde(with = "Goal__PredicateDef")]
-      &'a solve::Goal<'tcx, ty::Predicate<'tcx>>,
-    );
-    // TODO remove after deubbing
-    let debug_comparison = format!("{:?}", goal.predicate.kind().skip_binder());
     let necessity = infcx.guess_predicate_necessity(&goal.predicate);
     let num_vars =
       serialize::var_counter::count_vars(infcx.tcx, goal.predicate);
-    let goal = serialize_to_value(infcx, &Wrapper(goal))
+    let goal_value = serialize_to_value(infcx, &GoalPredicateDef(*goal))
       .expect("failed to serialize goal");
+
     Self {
-      goal,
+      goal: goal_value,
       result,
-      debug_comparison,
       necessity,
       num_vars,
+      is_lhs_ty_var: goal.predicate.is_lhs_ty_var(),
+
+      #[cfg(debug_assertions)]
+      debug_comparison: format!("{:?}", goal.predicate.kind().skip_binder()),
     }
   }
 }

crates/argus/src/serialize/const.rs

@@ -170,44 +170,60 @@ impl ParamConstDef {
 #[cfg_attr(feature = "testing", derive(TS))]
 #[cfg_attr(feature = "testing", ts(export, rename = "UnevaluatedConst"))]
 #[serde(tag = "type")]
-enum UnevaluatedConstKind<'tcx> {
-  ValuePath { data: path::ValuePathWithArgs<'tcx> },
-  AnonSnippet { data: String },
+enum UnevaluatedConstDef<'tcx> {
+  ValuePath {
+    data: path::ValuePathWithArgs<'tcx>,
+  },
+  AnonSnippet {
+    data: String,
+  },
+  AnonLocation {
+    #[serde(with = "SymbolDef")]
+    #[cfg_attr(feature = "testing", ts(type = "Symbol"))]
+    krate: Symbol,
+
+    path: path::BasicPathNoArgs<'tcx>,
+  },
 }
 
-impl<'tcx> From<&UnevaluatedConst<'tcx>> for UnevaluatedConstKind<'tcx> {
-  fn from(value: &UnevaluatedConst<'tcx>) -> Self {
+impl<'tcx> UnevaluatedConstDef<'tcx> {
+  fn new(value: &UnevaluatedConst<'tcx>) -> Self {
     let infcx = get_dynamic_ctx();
     let UnevaluatedConst { def, args } = value;
     match infcx.tcx.def_kind(def) {
-      DefKind::Const | DefKind::AssocConst => UnevaluatedConstKind::ValuePath {
+      DefKind::Const | DefKind::AssocConst => Self::ValuePath {
         data: path::ValuePathWithArgs::new(*def, args),
       },
       DefKind::AnonConst => {
         if def.is_local()
           && let span = infcx.tcx.def_span(def)
           && let Ok(snip) = infcx.tcx.sess.source_map().span_to_snippet(span)
         {
-          UnevaluatedConstKind::AnonSnippet { data: snip }
+          Self::AnonSnippet { data: snip }
         } else {
-          todo!()
+          // Do not call `print_value_path` as if a parent of this anon const is an impl it will
+          // attempt to print out the impl trait ref i.e. `<T as Trait>::{constant#0}`. This would
+          // cause printing to enter an infinite recursion if the anon const is in the self type i.e.
+          // `impl<T: Default> Default for [T; 32 - 1 - 1 - 1] {`
+          // where we would try to print `<[T; /* print `constant#0` again */] as Default>::{constant#0}`
+          Self::AnonLocation {
+            krate: infcx.tcx.crate_name(def.krate),
+            path: path::BasicPathNoArgs::new(*def),
+          }
         }
       }
       defkind => panic!("unexpected defkind {:?} {:?}", defkind, value),
     }
   }
-}
 
-pub struct UnevaluatedConstDef;
-impl UnevaluatedConstDef {
-  pub fn serialize<'tcx, S>(
+  pub fn serialize<S>(
     value: &UnevaluatedConst<'tcx>,
     s: S,
   ) -> Result<S::Ok, S::Error>
   where
     S: serde::Serializer,
   {
-    UnevaluatedConstKind::from(value).serialize(s)
+    Self::new(value).serialize(s)
   }
 }
 

crates/argus/src/serialize/mod.rs

@@ -170,15 +170,42 @@ define_helper!(
 
 pub(crate) mod safe {
   use rustc_hir::def_id::DefId;
+  use rustc_trait_selection::traits::solve;
+  #[cfg(feature = "testing")]
+  use ts_rs::TS;
 
   use super::*;
 
   #[derive(Serialize)]
-  pub struct PathDefNoArgs(#[serde(with = "path::PathDefNoArgs")] pub DefId);
+  #[cfg_attr(feature = "testing", derive(TS))]
+  #[cfg_attr(feature = "testing", ts(export))]
+  #[cfg_attr(feature = "testing", ts(rename = "GoalPredicateDefSafeWrapper"))]
+  pub struct GoalPredicateDef<'tcx>(
+    #[serde(with = "ty::Goal__PredicateDef")]
+    #[cfg_attr(feature = "testing", ts(type = "GoalPredicate"))]
+    pub solve::Goal<'tcx, rustc_ty::Predicate<'tcx>>,
+  );
+
+  #[derive(Serialize)]
+  #[cfg_attr(feature = "testing", derive(TS))]
+  #[cfg_attr(feature = "testing", ts(export))]
+  #[cfg_attr(feature = "testing", ts(rename = "PathDefNoArgsSafeWrapper"))]
+  pub struct PathDefNoArgs(
+    #[serde(with = "path::PathDefNoArgs")]
+    #[cfg_attr(feature = "testing", ts(type = "PathDefNoArgs"))]
+    pub DefId,
+  );
 
   #[derive(Serialize)]
+  #[cfg_attr(feature = "testing", derive(TS))]
+  #[cfg_attr(feature = "testing", ts(export))]
+  #[cfg_attr(
+    feature = "testing",
+    ts(rename = "TraitRefPrintOnlyTraitPathDefSafeWrapper")
+  )]
   pub struct TraitRefPrintOnlyTraitPathDef<'tcx>(
     #[serde(with = "ty::TraitRefPrintOnlyTraitPathDef")]
-    pub  rustc_ty::TraitRef<'tcx>,
+    #[cfg_attr(feature = "testing", ts(type = "TraitRefPrintOnlyTraitPath"))]
+    pub rustc_ty::TraitRef<'tcx>,
   );
 }

crates/argus/src/serialize/path/mod.rs

@@ -62,6 +62,18 @@ impl<'tcx> ValuePathWithArgs<'tcx> {
   }
 }
 
+#[derive(Serialize)]
+#[cfg_attr(feature = "testing", derive(TS))]
+#[cfg_attr(feature = "testing", ts(export))]
+// Useful in scenarios when using a `ValuePathXXX` would cause the
+// pretty printer to enter an infinite loop.
+pub struct BasicPathNoArgs<'tcx>(DefinedPath<'tcx>);
+impl<'tcx> BasicPathNoArgs<'tcx> {
+  pub fn new(def_id: DefId) -> Self {
+    Self(PathBuilder::compile_value_path(def_id, &[]))
+  }
+}
+
 #[derive(Serialize)]
 #[cfg_attr(feature = "testing", derive(TS))]
 #[cfg_attr(feature = "testing", ts(export))]

ide/packages/extension/src/ctx.ts

@@ -392,11 +392,7 @@ class BackendCache {
 
     // NOTE: the returned value should be an array of a single tree, however,
     // it is possible that no tree is returned. (Yes, but I'm working on it.)
-    const tree = _.filter(res.value, t => t !== undefined) as Array<
-      SerializedTree | undefined
-    >;
-
-    const tree0 = tree[0];
+    const tree0 = _.compact(res.value)[0];
     if (tree0 === undefined) {
       return;
     }

ide/packages/panoptes/src/TreeView/BottomUp.tsx

@@ -3,34 +3,70 @@ import _ from "lodash";
 import React, { useContext } from "react";
 
 import { TreeContext } from "./Context";
-import { DirRecursive } from "./Directory";
+import { CollapsibleElement, DirRecursive } from "./Directory";
 
 const BottomUp = () => {
   const tree = useContext(TreeContext)!;
-  const leaves = _.map(tree.errorNodes(), leaf => {
+  const getParent = (idx: ProofNodeIdx) => {
+    let p = tree.parent(idx);
+    return p !== undefined ? [p] : [];
+  };
+
+  const leaves = _.map(tree.errorNodesRecommendedOrder(), leaf => {
     let curr: ProofNodeIdx | undefined = leaf;
     while (curr !== undefined && !("Goal" in tree.node(curr))) {
       curr = tree.parent(curr);
     }
     return curr;
   });
 
-  const getParent = (idx: ProofNodeIdx) => {
-    let p = tree.parent(idx);
-    return p !== undefined ? [p] : [];
+  // The "Argus recommended" errors are shown expanded, and the
+  // "others" are collapsed. Argus recommended errors are the ones
+  // that failed or are ambiguous with a concrete type on the LHS.
+  const [argusRecommended, others] = _.partition(_.compact(leaves), leaf => {
+    const node = tree.node(leaf);
+    if ("Goal" in node) {
+      const goal = node.Goal.data;
+      return (
+        goal.result === "no" ||
+        goal.result === "maybe-overflow" ||
+        !goal.isLhsTyVar
+      );
+    } else {
+      // Leaves should only be goals...
+      return false;
+    }
+  });
+
+  const LeafElement = ({ leaf }: { leaf: ProofNodeIdx }) => {
+    return (
+      <DirRecursive level={[leaf]} getNext={getParent} styleEdges={false} />
+    );
   };
 
-  return _.map(leaves, (leaf, i) =>
-    leaf === undefined ? (
-      ""
-    ) : (
-      <DirRecursive
-        key={i}
-        level={[leaf]}
-        getNext={getParent}
-        styleEdges={false}
+  const recommended = _.map(argusRecommended, (leaf, i) => (
+    <LeafElement key={i} leaf={leaf} />
+  ));
+
+  const fallbacks =
+    others.length === 0 ? null : (
+      <CollapsibleElement
+        info={<span>Other failures ...</span>}
+        Children={() => (
+          <>
+            {_.map(others, (leaf, i) => (
+              <LeafElement key={i} leaf={leaf} />
+            ))}
+          </>
+        )}
       />
-    )
+    );
+
+  return (
+    <>
+      {recommended}
+      {fallbacks}
+    </>
   );
 };
 

ide/packages/panoptes/src/TreeView/TopDown.tsx

@@ -1,4 +1,4 @@
-import { ProofNodeIdx } from "@argus/common/bindings";
+import { Candidate, Goal, ProofNodeIdx } from "@argus/common/bindings";
 import _ from "lodash";
 import React, { useContext } from "react";
 
@@ -7,7 +7,42 @@ import { DirRecursive } from "./Directory";
 
 const TopDown = () => {
   const tree = useContext(TreeContext)!;
-  const getChildren = (idx: ProofNodeIdx) => tree.children(idx);
+
+  const getGoalChildren = (kids: ProofNodeIdx[]) => {
+    // Sort the candidates by the #infer vars / height of the tree
+    return _.sortBy(kids, k => {
+      const inferVars = tree.inferVars(k);
+      const height = tree.maxHeigh(k);
+      return inferVars / height;
+    });
+  };
+
+  const getCandidateChildren = (kids: ProofNodeIdx[]) => {
+    return _.sortBy(kids, k => {
+      switch (tree.result(k) ?? "yes") {
+        case "no":
+          return 0;
+        case "maybe-overflow":
+          return 1;
+        case "maybe-ambiguity":
+          return 2;
+        case "yes":
+          return 3;
+      }
+    });
+  };
+
+  const getChildren = (idx: ProofNodeIdx) => {
+    const node = tree.node(idx);
+    const kids = tree.children(idx);
+    if ("Goal" in node) {
+      return getGoalChildren(kids);
+    } else if ("Candidate" in node) {
+      return getCandidateChildren(kids);
+    } else {
+      return [];
+    }
+  };
   return (
     <DirRecursive level={[tree.root]} getNext={getChildren} styleEdges={true} />
   );