Recursive calls fail to infer

FStarLang / steel

The Steel separation logic library for F*

Apache License 2.0

31 stars 5 forks source link

Recursive calls fail to infer #141

Closed nikswamy closed 10 months ago

nikswamy commented 11 months ago

fn rec loop (#t:Type0) (l:list t)
requires emp
ensures emp
{
  loop #t l;
}

Leaving out the #t produces the error:

prover-error: Ill-typed substitution

nikswamy commented 11 months ago

The recursively bound loop is introduced at an odd type. Notice that it takes a type parameter t' but the type of the second argument refers to the outer t#1.

In typing environment: [loop#3 : (#t'#192:Type -> Tot (l'#194:(Prims.list t#1) -> Tot (((Pulse.Lib.Core.stt Prims.unit) Pulse.Lib.Core.emp) (fun x#224 -> (Pulse.Lib.Core.emp $$ (residual) Prims.Tot Pulse.Lib.Core.vprop))))), l#2 : (Prims.list t#1), t#1 : Type]