Inference in presence of 'error'

[monoidal]

I'd expect this to typecheck:

f :: a ->. b
f x = error "bad" x

We don't fully support inference yet, but this one contains merely application, no lambdas or case. Workaround: f x = (error "bad" :: a ->. b) x.

The fix could be guarded on LinearTypes, as in #379.

[monoidal]

A different example I expected to typecheck is map Just written as:

m :: [a] ->. [Maybe a]
m [] = []
m (x:xs) = Just x : m xs

Just has to be written as (Just :: a ->. Maybe a). This sounds like a consequence of the p * q = Omega rule.

[aspiwack]

The first example is ok, for now. The second breaks linear base, probably. It's bad.

[monoidal]

After a discussion, for now let's restore the a * b <= c rule, making a * b and sup a b the same thing. This means, revert #360 and #351. Also, add a rule in mkMultSup. This is best done after merging #386, where tcSubMult behaves sensibly. This should (1) fix this issue, (2) help in tweag/linear-base#38 (3) address the concerns about violating the substitution invariant in Multiplicity.hs.

[monoidal]

WIP on krzysztof/family, fails Lint:

<no location info>: warning:
    In the pattern of a case alternative: (I# dt_a8Vi :: Int#)
    Linearity failure in variable: dt_a8Vi
    'Omega ⊈ MultMul 'Omega 'Omega

[aspiwack]

Lint it supposed to be aware of this rule. We need to implement it in the submultiplicity check that lint does. (there used to be a submultiplicity predicate in Mult.hs. It was taking care of this)

[monoidal]

The map Just example was fixed by #391.

Remaining work:

• Use reduceTyFamApp_maybe in Lint (left as TODO in Add MultMul family back #391) -> moved to Use reduceTyFamApp_maybe in Lint #500.
• Fix the original problem with error, which turned out not to be related.

[monoidal]

Likely culprit: let unif_fun_ty = mkVIsFunTyOm arg_tys res_tys in TcUnify, function matchActualFunTysPart.

[monoidal]

Moved to upstream:#18731.