Type errors about linearity are unhelpful
The problem
Error messages involving linear types can be extraordinarily unhelpful at times.
> let f :: Maybe a %1 -> Maybe (a, a); f x = case x of { Just y -> Just (y,y); Nothing -> Nothing }
<interactive>:3:40: error: [GHC-18872]
• Couldn't match type ‘Many’ with ‘One’
arising from multiplicity of ‘x’
• In an equation for ‘f’:
f x
= case x of
Just y -> Just (y, y)
Nothing -> Nothing
Why is the multiplicity of x
inferred to be Many
? Well, it's because the case
is inferred to be Many
. Because y
is used twice in the right-hand side of the first alternative. The type of the function may tip you off, but what about this one:
> let f :: Maybe a %1 -> Maybe a; f x = case x of { ~(Just y) -> Just y ; Nothing -> Nothing }
<interactive>:4:35: error: [GHC-18872]
• Couldn't match type ‘Many’ with ‘One’
arising from multiplicity of ‘x’
• In an equation for ‘f’:
f x
= case x of
~(Just y) -> Just y
Nothing -> Nothing
Do you know out of the top of your head what's going on here? It turns out that lazy patterns are always unrestricted. When it happens in a larger function, it can get really hard to pinpoint where the problem happens (even for me, who wrote most of the linear type checking…).
I'm not satisfied with it. I never was, but as I'm finishing with linear lets #18461 (closed) , I feel this is the last big hurdle for adoption. So I want to tackle these error messages.
How do we go about it?
This issue has two parts. Two questions really.
- What should error messages look like?
- How do we realise this technically within the constraints of GHC.
Error messages
I do have some idea of what I want the error messages to look like. I'd like the trace to contain messages like
• The multiplicity of ‘x’ was scaled by ‘Many’ because lazy patterns are always unrestricted in: ~(Just y)
in addition (and before) the location context
There are many such places, some will be easier to document than others. I imagine that we'll increase the precision of the error messages incrementally.
Technical approach
There I'm not entirely clear. Where could we attach this context? In the UsageEnv
which records all the inferred multiplicities, maybe?
One thing to keep in mind: if we are to catch these “lazy pattern” situation: at the time we do this, we're not modifying the UsageEnv
, we're unifying the multiplicity annotation on the case
, therefore, we will probably need a way to register such unifications to the proper variables (all the variables in the closure of the scrutiny!).
@monoidal @treeowl @alt-romes you may have opinions or ideas to share there.
@simonpj, @rae if you have insight in the type-checker's architecture, please share.