FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.69k stars 232 forks source link

Pattern does not contain all quantified variables even for trivial inductive types after new_effect_for_free with actions #812

Open catalin-hritcu opened 7 years ago

catalin-hritcu commented 7 years ago

I'm getting annoying warnings (especially annoying in interactive mode during class!) of this form:

WARNING: (63889,7): pattern does not contain all quantified variables.

even for trivial inductive types like this

type arg =
| Bool | Int | Char | String
catalin-hritcu commented 7 years ago

OK, reproducing in a clean state this is not as easy as I thought. It seems to be enabled by a preceding new_effect_for_free with an action:

[...]
reifiable reflectable new_effect_for_free {
  XEXN : (a:Type) -> Effect
  with repr     = ex
     ; bind     = bind_ex
     ; return   = return_ex
  and effect_actions
       raise   = raise_ex
}

type arg =
| Bool | Int

So probably not exactly what I was seeing in class.