Tests for type errors

[adamgundry]

It occurred to me that the test suite could do with a more thorough set of tests for the type errors that are generated by invalid code, to prevent error message regressions. We could either do this with doctests, or use -fdefer-type-errors and catch and inspect type errors at runtime.

[phadej]

It's tricky.

*Optics.Core> :set -fdefer-type-errors 
*Optics.Core> let x = 'x' + True

<interactive>:2:15: warning: [-Wdeferred-type-errors]
    • Couldn't match expected type ‘Char’ with actual type ‘Bool’
    • In the second argument of ‘(+)’, namely ‘True’
      In the expression: 'x' + True
      In an equation for ‘x’: x = 'x' + True
*Optics.Core> x
*** Exception: <interactive>:2:15: error:
    • Couldn't match expected type ‘Char’ with actual type ‘Bool’
    • In the second argument of ‘(+)’, namely ‘True’
      In the expression: 'x' + True
      In an equation for ‘x’: x = 'x' + True
(deferred type error)

but

*Optics.Core> let xs = view folded "foobar"

<interactive>:4:10: warning: [-Wdeferred-type-errors]
    • A_Fold cannot be used as A_Getter
      Perhaps you meant one of these:
        ‘traverseOf_’ (from Optics.Fold)
        ‘foldMapOf’ (from Optics.Fold)
        ‘toListOf’ (from Optics.Fold)
        ‘(^..)’ (from Optics.Operators)
    • In the expression: view folded "foobar"
      In an equation for ‘xs’: xs = view folded "foobar"
*Optics.Core> xs
*** Exception: unreachable
CallStack (from HasCallStack):
  error, called at src/Optics/Internal/Optic/Subtyping.hs:40:15 in optics-core-0.3-inplace:Optics.Internal.Optic.Subtyping

We reach unreachable:

optics/optics-core/src/Optics/Internal/Optic/Subtyping.hs

Lines 34 to 40 in a47f004

	-- | Overlappable instance for a custom type error.
	instance {-# OVERLAPPABLE #-} TypeError
	('ShowType k ':<>: 'Text " cannot be used as " ':<>: 'ShowType l
	':$$: 'Text "Perhaps you meant one of these:"
	':$$: ShowEliminations (EliminationForms k)
	) => Is k l where
	implies _ = error "unreachable"

We need a support in GHC to scrutinize on empty dictionary, compare EmptyCase vs. error "this should not happen".

In other words, We should be able to write something like

foo :: (Int ~ Char) => Void
foo ()

or

bar :: TypeError ('Text "err") => Void
bar ()

where syntax is Agda-inspired. We probably need something of bar = ... form, but I have no ideas. I haven't checked whether there is GHC issue about this.

[adamgundry]

For future reference: https://gitlab.haskell.org/ghc/ghc/-/issues/18310 is the GHC issue this ticket inspired.