assertions to create new type checking rules

[fnoble]

e.g.

lol = seqList [
  FnDef "lol" (FnT [("a", IntType), ("b", IntType)] [
    ("va", VecType ["a"] NumType),
    ("vb", VecType ["b"] NumType)
    ] Void) $ seqList [
      assert $ "a" == 2 * "b",    -- Should allow the type checker to use the rule 
                                  -- a = 2b and insert an assertion into the generated C
      "va" := "vb" :# "vb"
    ]
 ]

[kovach]

in this case, should the type signature just be
...("va", VecType [2 * "b"] NumType)...

I'd like to have invariants like this enforced by the type system whenever possible.

[fnoble]

Yes, this is a simple example but I think there are cases when you don't want to do this.