Internal consistency of saw-core typechecking

[robdockins]

It's hard for me to track things through the typechecker, but it doesn't appear that Pi types collapse into Prop when the conclusion is in Prop, as I would expect. Instead it seems to follow the same rules as the predicative sort tower.

For example, the type assigned to (x : Bool) -> Eq Bool x x is sort 0 even though Eq is in Prop. Likewise the type of (A:sort 0) -> (x:A) -> Eq A x x is sort 1.

Related question regarding EqTrue. Why is it defined in sort 1?

EqTrue : Bool -> sort 1;
EqTrue x = Eq Bool x True;

[eddywestbrook]

That is very strange. Here is the line that computes the sort of a pi type:

https://github.com/GaloisInc/saw-core/blob/master/saw-core/src/Verifier/SAW/SCTypeCheck.hs#L402

It looks like it is checking whether the output type is a Prop, and, if so, is returning Prop.

[eddywestbrook]

I am guessing that EqTrue is just old: until recently, Eq was defined as a sort 1.

[robdockins]

Interesting. Looks like that doesn't agree with the scTypeOf operator, which is mainly the one that is used in SAW.

https://github.com/GaloisInc/saw-core/blob/1dce64877bb720f48db9500ca1d399c6fc8a5e8e/saw-core/src/Verifier/SAW/SharedTerm.hs#L918

[eddywestbrook]

Doh! I guess I can claim some of the fault there. I wrote the current version of SCTypeCheck.hs, but I guess I didn't update scTypeOf. Sounds like a bug then?

[robdockins]

Looks like it. Easy enough to fix, I think.

Ensuring these functions stay in sync somehow... that's not so easy.

[eddywestbrook]

Yeah, I was just thinking about how one would do that. I could imagine modifying the TypeInfer class so that typeInfer takes a Bool flag for whether to do thorough checking or to just assume that the input is already type-correct? I dunno...

[robdockins]

The core issue was solved in GaloisInc/saw-core#190, but maybe we should keep this ticket open to discuss ways to keep the type-checking code in sync.