Failing verification conditions are shown as type-class resolution errors

[gebner]

module TypeErr
open Pulse
#lang-pulse

let fin (n: nat) = i:nat { i < n }

fn foo #k (r: ref (fin k)) (v: erased (fin (-10)))
  requires pts_to r v
  (*       ^^^^^^
  Could not solve typeclass constraint
    `has_pts_to (ref (fin k)) (erased (fin (- 10)))`
  *)
  ensures pts_to r v
{
  ()
}

This should ideally give an error on -10 instead.

[gebner]

This error also appears in pure F*. Apparently type class resolution is (a) run before sending the VCs to Z3 and (b) eagerly discharges VCs itself.

let bar #k (r: ref (fin k)) (v: erased (fin (-10))) =
  pts_to r v
(*^^^^^^
Could not solve typeclass constraint
    `has_pts_to (ref (fin k)) (erased (fin (- 10)))`
*)