can't inference type of a Nothing value

[YuMingLiao]

`
TutorialD (master/main): a :: {a Maybe Integer}

TutorialD (master/main): insert a relation{tuple{ a Nothing}}

ERR: TypeConstructorTypeVarMissing "a"
`

[agentm]

You are right that this is annoying lack of type inference, but you've hit this before in #254 which is a duplicate of #46. The workaround is to specify the type in the relation, but the long-term fix would be for the backend to deduce that the type of relation... can be deduced from the context of a. Currently, the relation... expression is type-checked in isolation.

[YuMingLiao]

A note: after looking into the code, I guess the type deduction and equality-check should happen in binary operations like union.

[agentm]

Yea, it's tricky. It might be possible to walk both sides of a union and then apply one set of type hints to the other side of the union, but perhaps a better strategy is to extract the relvar's type and not pass it down the union, or perhaps this is a special case for extracting type hints. It's a tough choice which is why I haven't jumped on a solution.

[YuMingLiao]

I would like to offer some thought about type deduction and type check here:
I guess it would be like a monoid thing. I mean:

relvar1 :: {a a}
relvar1 := relation{tuple{a bvalue :: b}, tuple{a cvalue :: c}, (dvalue :: d)} -- (dvalue :: d) here is an anonymous tuple for, maybe in the future, an easier way to type a tutd like {("A",1),("B",2)}

relvar2 :: {a e}

deducedType of attribute a in relvar1 = (a <> (b <> c <> D))
deducedType of attribute a in relvar2 in (relvar1 union relvar2) = (a <> (b <> c <> D)) <> e
So deducing relation types seems like a monoid thing, in theory.
If d is specified as D, then (a <> b <> c <> D <> e) = D if a, b, c and e can be D.

I believe this covers all the three cases you mentioned, and if any of the types is specified, that may be the best type to deduce to.