Required fields taken

[zilinc]

No description provided.

[liamoc]

Actually, this is not a bug, it's intended behaviour. The fix commit breaks soundness of the subtyping relation, so you'll want to revert that.

[liamoc]

You're allowed to "take" discardable fields from records as part of the subtyping relation now.

[zilinc]

type ExState
type RR c a b = (c, <Success a | Error b>)
type OSBuffer

type Ext2Superblock = {
    inode_count             : U32,
    magic                   : U16
}

deserialise_Ext2Superblock: (ExState, OSBuffer!, U32) -> RR ExState (Ext2Superblock, U32) ()

free_Ext2Superblock  : (ExState, Ext2Superblock take (..)) -> ExState
free_Ext2Superblock' : (ExState, Ext2Superblock) -> ExState

foo : #{ex: ExState, buf_super : OSBuffer} -> ExState
foo #{ex, buf_super} = 
  let (ex, res) = deserialise_Ext2Superblock (ex, buf_super, 0) !buf_super
  in res
  | Success (super, _) -> 
      free_Ext2Superblock (ex, super)  -- super is all-untaken
  | Error () -> ex

This exampled didn't typecheck before my last change. If you used free_Ext2Superblock' then it's OK. It reported that the fields of super were required but had been taken.

[zilinc]

reverted in ee00083

[zilinc]

@liamoc Still don't get why in tests/pass_ticket-e22-2.cogent the pattern var superof type ?11 is inferred to be Ext2Superblock take (..) instead of all untaken. In the case of tests/pass_ticket-e22-3.cogent, it causes the member op to fail.

[liamoc]

This is a separate bug than the previous one. I see why this is happening but I'm struggling to figure out a nice way to fix it. Basically, the free call is introducing a constraint like

 ?11 :< Ext2Superblock take (..)

And the member call only generates a constraint like:

 { magic : U16 } :>~ ?11

which is only checked once ?11 is resolved.

This may require me to design the solver quite differently. It'll need some serious thinking.

[liamoc]

OK, I think I've figured out the changes I need to make, although it's quite a significant amount of refactoring. Might take me a while.

[liamoc]

OK, If you want you can merge my tc-new branch. It fixes this bug.

I've gotten rid of those Partial or :<~ constraints entirely. Now we have just subtyping (and a separate constraint Upcastable specifically for integers).

Subtyping, however, is now a relation on type fragments, which may be:

• A TCType (a unification variable or a concrete type)
• A partially-specified variant type.
• A partially-specified record type.

This type is non-recursive, and we never instantiate type variables to type fragments (meaning that our substitution type still is effectively a map from variables to TCTypes). This guarantees that no partially-specified type will actually show up in the resultant program.

Now the solver will group regular and "partial" subtyping constraints together, and solve them together. This solves this bug as this bug is caused by the (non-partial) subtyping constraints being solved first -- then the partial constraints fail. We need to come up with solutions that satisfy all the constraints, and a solution that satisfies just the non-partial subtyping constraints will not be a safe solution for the partial ones.. hopefully that makes sense.

The code in the solver is now quite repetitive though, so if anyone wants to have a go at refactoring it (while preserving semantics) it might be a nice thing.

[liamoc]

OK, I'm in the process of writing up this algorithm now, and I realised there's probably still a bug here.

The general gist of the solver is that it groups subtyping constraints by their variable (and whether it occurs on the left or right hand side). So for example all constraints of the form ?x :< .... Then it computes the GLB (or LUB) of all the types on the other side to get the result.

The possible bug is that if there are flex-flex constraints, e.g ?x :< ?y, we currently don't include them in the constraint set and delay them until later. This means that it may be possible to find a program for which the flex-rigid constraints give a solution for ?x and ?y that doesn't satisfy that flex-flex constraint.

The fix is, if we have only one flex-rigid constraint ?x :< T, we should not apply the substitution x |-> T if there are flex-flex constraints ?x :< ?y still in the set.

Posting this mostly as a reminder to myself to try to fix this possible problem and see if it breaks anything. I haven't found an example program that breaks, but the algorithm may give surprising results, I'm not sure.

[liamoc]

OK, I've convinced myself that it's safe to delay flex-flex constraints.

Because, if we have a solution for ?x, we will substitute right away, so the ?x :< ?y constraint will become a flex-rigid ... :< ?y constraint which will inform solving for ?y. Because our subtyping relationship is basically a lattice, it shouldn't matter if ?x or ?y is solved first. So delaying until we solve either one is allowed.

Should we close this issue?

[zilinc]

No, the same symptom (... of type ... is required but has been taken) appears again in ext2. I'm still working on shrinking the code.

[zilinc]

type Result a b = <Success a | Error b>

type Option a
type WordArray a

type FsState = {
    superblock_num   : U32,
    flags            : U32,
    prealloc_offsets : Option (WordArray U32)
}

malloc_FsState: () -> Result (FsState take (..)) ()

wordarray_create : all (a :< DS). () -> Result (WordArray a) ()

free_FsState : FsState take (..) -> ()

fs_mount: () -> Result FsState U32
fs_mount _ =
    malloc_FsState ()
    | Success state_t -> 
        let state_t' = state_t { superblock_num = 1 }
         in wordarray_create ()
            | Success prealloc_offsets =>
                let state = state_t' {  -- state : ?10, state_t' : ?11
                      flags = 2,
                      prealloc_offsets = Some prealloc_offsets
                    }
                in Success state
            | Error _ ->
                let _ = free_FsState state_t'
                in Error 1
    | Error _ -> Error 2

Under d10fa13, the Unsat is from ?11 put (flags, prealloc_offsets) :< ?10.
It first infers variable state_t' in the failure case to be all taken due to the function free_FsState application. Then it (wrongly) concludes state_t' the binder to be all taken. Thus state has superblock_num field taken in the final result.

[liamoc]

Alright, I stepped through (a further simplified version of) this example, running the algorithm by hand. I figured out what's wrong. The constraints you end up with are something like:

   ?1 :< { a : U32, b : WordArray U32 } take b
   ?1 :< ?{a : U32}
   ?0 :< { a : U32, b : WordArray U32 } take (a, b)
   ?0 :< ?1 

In this scenario, the solver sees a "no-brainer" opportunity for ?0 that is not correct. I guess I was wrong when I said earlier that delaying flex-flex constraints is OK.

[liamoc]

OK, I've pushed a series of commits to my fork. Merge whenever. It passes all the pass_ tests (including one test that should never have been passing, but I fixed the test case).

Now it will not solve (i.e. generate a substitution for) any "no-brainer" constraint while there are still flex/flex constraints about the same variable (for this check we ignore reflexive constraints ?x :< ?x). We also make an exception here for numeric types. Seeing as, for numeric types, subtyping is just equality, we solve all subtyping no-brainers for numeric types before we try and guess the numeric types from the cast.

This doesn't seem to have caused any regressions.

I'm also working on better handling of constraints like

?x take f :< {...}

Now this transforms into:

?x :< {...} put f

And similar. I haven't finished all the rule cases for this yet, but it already seems to pass all the tests. I'm not sure how commonly these constraints come up so fully implementing this may not be urgent.

[liamoc]

After some testing, I think transforming ?x take f :< {...} to ?x :< {...} put f etc. is not needed. Seeing as I'm not convinced such transformations are sound in all cases, I removed it for now. Let me know if you run into incompleteness cases.

Now it will simply not solve any system of constraints involving such type operators until they can be evaluated.

Also, I've discovered a really simple way to explain how this algorithm works now which suggests I'm on the right track.