inkytonik / cooma

The Cooma project is investigating secure programming language design based on fine-grained object capabilities.
Mozilla Public License 2.0
3 stars 2 forks source link

Typing of case expressions is sensitive to ordering of cases #43

Closed nhweston closed 3 years ago

nhweston commented 3 years ago

I was running into some strange errors while trying to implement monadic error types. I finally figured out what the problem is.

Consider the following Cooma program:

{
    fun (x : <A : Int, B : String>, fa : (Int) Unit, fb : (String) Unit) {
        x match {
            case A(a) => fa(a)
            case B(b) => fb(b)
        }
    }
}

As expected, this program type checks with no errors.

I'll now make a small change to the way I've written this program. I'm going to swap the ordering of the cases:

{
    fun (x : <A : Int, B : String>, fa : (Int) Unit, fb : (String) Unit) {
        x match {
            case B(b) => fb(b)
            case A(a) => fa(a)
        }
    }
}

Of course, this should still type check.

Instead, we get the following error:

../sb/test.cooma:4:29:error: expected String, got b of type Int
            case B(b) => fb(b)
                            ^
../sb/test.cooma:5:29:error: expected Int, got a of type String
            case A(a) => fa(a)
                            ^

So it looks like what's happening is that the semantic analyser is expecting cases to appear in the same as they are defined in the variant.

Might this (from SemanticAnalyser.scala:570) be the culprit?:

case CaseValueEntity(tree.parent.pair(c, Mat(e, _))) =>
    tipe(e) match {
        case Some(VarT(r)) if tree.index(c) - 1 < r.length =>
            Some(r(tree.index(c) - 1).expression)
        case _ =>
            None
    }
inkytonik commented 3 years ago

Yes, you are right. I'd forgotten about this corner cutting :-) It should be fairly easy to fix. I'll take a look.