default Order dec

(* A function which is merely parametrised by a size does not need to be
   monomorphised *)

val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric

function parametric(n) = {
  let (bit['n]) x = exts(0x80000000) in
  extz(x)
}

(* But if we do a calculation on the size then we'll need to case split *)

val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends

function depends(n) = {
  let 'm = 2 * n in
  let (bit['m]) x = exts(0x80000000) in
  extz(x)
}

val unit -> bool effect pure run

function run () =
  parametric(32) == 0x0000000080000000 &
  parametric(64) == 0xffffffff80000000 &
  depends(16) == 0x0000000080000000 &
  depends(32) == 0xffffffff80000000