Begginner problem with error: "Computed type "" and effect "ALL" is not compatible with the annotated type " " effect "Tot""

[alex4482]

Hi again. i have received that error in the title.

and i also have a different problem. I 'translated' this function from haskell because i need to and i am still a beginner in F*, but in Haskell you could write 'error "message" ', and if the program would end up on that branch, it would throw an error. Is there and equivalent for this in F*? I am asking because i havent found one yet. (this is why i commented 2 lines in my function)

//edit
i just found 'failwith message', but now after i put it in my code, when i try to verify the code it says the same error as above. so i have 2 places where it appears
//

my function is this, it's a bit long and with many branches so i am sorry if its a problem, but maybe you could at least explain what that error means. I've encountered the opposite error (Tot in the place of ALL, and ALL in the place of Tot), but not this one.

val resoluteTwoClauses : clause -> clause -> literal -> guessLevel -> memory -> clause & guessLevel
let resoluteTwoClauses cl1 cl2 pivot conflictLevel m =
let firstLiterals = removeFromList (negateLit pivot) (getAllLiteralsFromClause cl1) in
let secondLiterals = removeFromList pivot (getAllLiteralsFromClause cl2) in
if firstLiterals = []
then
//if secondLiterals = []
// then error "error at resolution of 2 clauses"
//else
if (length secondLiterals) = 1
then (Lit (hd secondLiterals), 0)
else
let highestLevelBelowConflict = getHighestLevelBelowConflict secondLiterals conflictLevel m in
let newClause = makeClauseFromLiterals secondLiterals in
(newClause, highestLevelBelowConflict)
else
if secondLiterals = []
then
if (length firstLiterals) = 1
then (Lit (hd firstLiterals), 0)
else
let newClause = makeClauseFromLiterals firstLiterals in
let highestLevelBelowConflict = getHighestLevelBelowConflict firstLiterals conflictLevel m in
(newClause, highestLevelBelowConflict)
else
let bothClauseLiterals = append secondLiterals firstLiterals in
let newClause = makeClauseFromLiterals bothClauseLiterals in
let highestLevelBelowConflict = getHighestLevelBelowConflict bothClauseLiterals conflictLevel m in
(newClause, highestLevelBelowConflict)

[aseemr]

Hi @alex4482:

The type clause -> clause -> literal -> guessLevel -> memory -> clause & guessLevel is a shorthand for clause -> clause -> literal -> guessLevel -> memory -> Tot (clause & guessLevel). Notice the Tot annotation at the result type. This means that F* expects the function to be total and without any side-effects.

If you want to write effectful code, e.g. that throws exceptions, you need to annotate the type as such, e.g. you could say: clause -> clause -> literal -> guessLevel -> memory -> ML (clause & guessLevel), where ML is an effect that allows divergence, state, and exception.

There are other refinements of ML you could use, e.g. All that allows for writing pre- and postconditions (see ulib/FStar.All.fst). But to begin with perhaps you could port your code using ML and then refine it gradually.

(Also, I could not run F* on your code snippet to see the actual error. If you could post self-contained examples, or links to them, then we can try to reproduce the error ourselves and provide better feedback.)

[nikswamy]

Another tip @alex4482

You can format your code as a literal block in markdown by placing it within a triple quote block.

like so

See https://markdown.land/markdown-code-block

[klinvill]

You can also enable syntax highlighting by putting fstar after the leading triple quote (e.g. ```fstar)

[nikswamy]

Also, recall that unlike Haskell, total functions in F* are really total mathematical functions: they can't raise errors, do IO etc.

This makes "printf-debugging" for total functions a little tricky.
If you really need to print things in a total function, F* provides an unsound escape hatch: See FStar.IO.debug_print_string.

[alex4482]

woow thanks. I saw that the 'default' declaration of a function is also a total function. If i had known how to 'declare' another type of function I would have done so.