Test unary operators that don't typecheck

[ggreif]

This keeps track of rejected type/unop combinations.

There is some wonkiness going on with +/Nat, which I'll tackle next.

UPDATE (12-09-2019): This PR only tests the status quo.
There have been some changes to the coverage checker and its interaction with type checking, so that previously described problems seem to be resolved.

[ggreif]

Of course, this error is not very convincing...

[rossberg]

That is intentional, though. Nat doesn't have any notion of sign.

[ggreif]

dito

[rossberg]

That is intentional, though. Nat doesn't have any notion of sign.

[ggreif]

@rossberg While I am behind the second phrase in

That is intentional, though. Nat doesn't have any notion of sign.

I am not sure I agree with the first. Here we don't talk about signs, but operators:

• ^ flips the bits for Words
• - flips the sign for Ints (Nats are Ints too by subtyping)
• + preserves the value (of Ints, thus Nats too by subtyping).

If -/+ would mean sign then wouldn't --5 be a somewhat weird construct? Dito for -+4?

[rossberg]

If you prefer, it's a sign modification operator. In patterns I'd view it as strictly a sign.

• + preserves the value (of Ints, thus Nats too by subtyping).

Technically, not for Nats, because you don't get back a Nat.

[ggreif]

Technically, not for Nats, because you don't get back a Nat.

@rossberg but that's only due to a type-system hack (in typing.ml around lines 489, 934)

    (* Special case for subtyping *)
    let t = if t1 = T.Prim T.Nat then T.Prim T.Int else t1 in

which changes - : Nat -> Nat to - : Nat -> Int, and same for +. This should be more restrictive and only apply to -. Then + would be a proper identity.

[rossberg]

It's not a type system hack but an implementation hack in the implementation of subsumption vs overloading. The declarative rule is very simple:

C |- exp : t
t in types(unop)
-----------------
C |- unop exp : t

where types(unop) is the set of types that unop is overloaded for.

It would become a type system hack if the rule was specialised to a specific operator.

[nomeata]

I see there is some discussion, but the diff is just a test case documenting the status quo (good), and some exception catching that makes the coverage checker not trip over if run on non-well-typed code, so I think we can merge this and work on the related issues elsewhere.

[rossberg]

I don't quite agree, see comment.

[ggreif]

Place the goods on the right case.

[ggreif]

Not sure where the Int is coming from, at least the parser isn't it:

$ src/asc -dp
ActorScript 0.1 interpreter
> let a = ^3;
(BlockE (LetD (VarP a) (UnE ??? NotOp (LitE (PreLit 3 Nat)))))
stdin:1.9-1.11: type error, operator is not defined for operand type
  Int

[rossberg]

Nit: I find the strings slightly confusing, especially when it says "good" for a negative case. Also, you probably should return (), or wrap the thing into an ignore like below, to rule out unrelated errors.

[ggreif]

I have confused myself too, so you are not alone. The rule of thumb is that when testing the switch expression in the REPL, I either expect "good" or a type error (as stated in the .ok file). Since ()-related type errors come out differently, we'll notice soon enough. I'll add a comment.

[rossberg]

Since ()-related type errors come out differently, we'll notice soon enough.

But that doesn't help the reader, because they'd have to look at a different file to figure out which one is intended. For clarity and hygiene, negative cases should only contain the errors that they are meant to test.