val bind (a: Type u#aa) (b: Type u#bb) (i1 i2: int) (f: repr a i1) (g: (x: a -> repr b i2))
    : Tot (repr b (i1 + i2))
val bind (a: Type u#aa) (b: Type u#bb) (i1 i2: int) (f: repr a i1) (g: (x: a -> repr b i2))
    : Tot (repr b (i1 + i2))
let bind (a:Type u#aa) (b : Type u#bb) (i1 i2 : int)
    (f : repr a i1)
    (g : (x:a -> repr b i2))
    : Tot (repr b (i1+i2)) =
    raise_val (i1+i2)
module Degenerate

open FStar.Universe

(* otherwise it's eqtype and strict checking fails *)
let int : Type u#0 = int

(* An effect which does not use its type *)

let repr (a:Type u#aa) (i:int) : Type u#aa =
  raise_t (x:int{x==i})

let return (a:Type u#aa) (x:a) : repr a 0 =
  raise_val 0
/
prims.fst.checked FStar.Universe.fsti.checked FStar.Pervasives.fsti.checked
Degenerate.fst

    a: Type ->
    b: Type ->
    i1: Degenerate.int ->
    i2: Degenerate.int ->
    f: Degenerate.repr a i1 ->
    g: (x: a -> Degenerate.repr b i2)
  -> Degenerate.repr b (i1 + i2)
Degenerate.int Degenerate.repr FStar.Universe.raise_val Prims.eq2 Prims.op_Addition
let bind (a: Type u#aa) (b: Type u#bb) (i1 i2: int) (f: repr a i1) (g: (x: a -> repr b i2))
    : Tot (repr b (i1 + i2)) =
  
raise_val (i1 + i2)