Pulse expects type constructors to be injective

[gebner]

The following is code that works in F*, but not in Pulse:

module Natlt
open Pulse.Nolib
#lang-pulse

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

let works #n (x: natlt n -> bool) (i: nat { i < n }) =
  let a: (natlt i -> bool) = x in
  ()

fn doesnt_work #n (x: natlt n -> bool) (i: nat { i < n }) {
  let a: (natlt i -> bool) = x;
  ()
}

Looking at the debugging output, the core type checker produces the guard forall (_: Natlt.natlt i). i == n which is obviously not provable.

[nikswamy]

thanks for the small repro. I'll take this