Kind inference checking problem for mutable tuples

[benl]

Added by Jared

The following function fails to compile.

example :: (Int, Int) %r0
        :- Mutable %r0
example = (0,0)

The error message is

ddc: src/Source/Desugar.hs:(647,4)-(670,28): Non-exhaustive patterns in case

The same error occurs if the region is placed before the type.

[benl]

This should be a parse error. To give the type of a mutable tuple use:

example :: Tuple2 %r0 Int Int 
        :- Mutable %r0

I'm not sure if we should support the sugar:

  (Int, Int) %r0

because the arguments are in the wrong order..

[erikd]

On the mailing list Ben said:

    This test really does have a kind error.

    With

       example :: (Int, Int) %r0
            :- Mutable %r0
       example = ( 0,0)


    compiling with -dump-desugar shows it gets desugared to:

    [Test.example]
           :: (Data.Tuple.Tuple2 Base.Int32 Base.Int32) %r0
            :- Base.Mutable %r0;

    Test.example
     =      Data.Tuple.Tuple2 (0i32) (0i32);


    And the expression:
    (Data.Tuple.Tuple2 Base.Int32 Base.Int32) %r0

    after type elaboration turns into:
   (Data.Tuple.Tuple2 %r1 (Base.Int32 %r2) (Base.Int32 %r3)) %r0

    This is miskinded, because Tuple2 has an extra region argument (%r0)

    .. so the bug is really another instance of DDC lacking proper kind
    inference / checking, and is related to #68.