GitLab

Summary

Writing a typed hole with linear arguments in scope gives spurious linearity errors. It does not help that these errors are display first, so that in ghcid, for instance, we may not even be able see the type of the hole.

Steps to reproduce

{-# LANGUAGE LinearTypes #-}

f :: Int #-> Bool #-> Char
f x y = _

Raises the following error:

<interactive>:15:31: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘x’
    • In an equation for ‘f’: f x y = _

<interactive>:15:33: error:
    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘y’
    • In an equation for ‘f’: f x y = _

<interactive>:15:37: error:
    • Found hole: _ :: Char
    • In the expression: _
      In an equation for ‘f’: f x y = _
    • Relevant bindings include
        y :: Bool (bound at <interactive>:15:33)
        x :: Int (bound at <interactive>:15:31)
        f :: Int #-> Bool #-> Char (bound at <interactive>:15:29)
      Valid hole fits include
        maxBound :: forall a. Bounded a => a
          with maxBound @Char
          (imported from ‘Prelude’ (and originally defined in ‘GHC.Enum’))
        minBound :: forall a. Bounded a => a
          with minBound @Char
          (imported from ‘Prelude’ (and originally defined in ‘GHC.Enum’))

Notice the two multiplicity errors at the top. Which are caused by the fact that the typechecker considers that _ counts for 0 use of x and y (where it ought to be: an unknown number of uses).

Expected behavior

Contrast the behaviour of _ with the behaviour of an empty case:

f :: Int #-> Bool #-> Char
f x y = () & \case {}

This compiles without a type error.

So holes should treat multiplicities exactly how a case {} would. After all, it's more or less the same idea: _ uses x and y an unknown number of times, and \case {} consumes x and y an arbitrary number of times. Since we don't know how many x-s and y-s are in _, we don't want to complain about it, so it's natural to approximate _ to be consuming x and y an arbitrary number of times.

Environment

• GHC version used: current master