Deferred type errors are too lazy, and can be dropped by Core optimisations

The mechanism for deferring type errors doesn't force the errors, meaning that programs that should fail with a deferred type error at runtime can be run without any errors. Consider the following example (from @rae):

{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}

module Main where

h :: Show (Int -> Int) => Int -> Int
h x = x

j :: Int
j = h 5

main :: IO ()
main = print j

./Main
5

This program runs without error, when one would have expected a type error about a missing Show (Int -> Int) instance. Richard points out that this can be a genuine security concern, for instance if constraints are used to ensure certain preconditions; a code-path that contains a type error can get run anyway!

The crux of the matter is that the evidence for Show (Int -> Int) is lifted:

h :: Show (Int -> Int) => Int -> Int
h = \ ($dShow :: Show (Int -> Int)) (x :: Int) -> x

j :: Int
j = let {
      $dShow :: Show (Int -> Int)
      $dShow
        = typeError @LiftedRep @(Show (Int -> Int))
            "error:\n\
            \    * No instance for (Show (Int -> Int)) arising from a use of `h'\n\
            \        (maybe you haven't applied a function to enough arguments?)\n\
            \    * In the expression: h 5\n\
            \      In an equation for `j': j = h 5\n\
            \(deferred type error)"# } in
    h $dShow (I# 5#)

As $dShow is not forced in j, and is unused in h, Core optimisations drop the type error, resulting in

j :: Int
j = I# 5#

Note that this problem doesn't arise for equality constraints, because their evidence is unlifted. For instance:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}

module Main where

h2 :: Int ~ Bool => Int -> Int
h2 x = x

j2 :: Int
j2 = h2 5

main :: IO ()
main = print j2

./Main
Main: Main.hs:11:6: error:
    * Couldn't match type `Int' with `Bool' arising from a use of `h2'
    * In the expression: h2 5
      In an equation for `j2': j2 = h2 5
(deferred type error)

This is because Int ~# Bool is unlifted, meaning that we must case on it in Core:

h2 :: (Int ~ Bool) => Int -> Int
h2 = \ ($d~:: Int ~ Bool) (x :: Int) -> x

j2 :: Int
j2
  = case typeError @(TupleRep []) @(Int ~# Bool)
           "error:\n\
           \    * Couldn't match type `Int' with `Bool' arising from a use of `h2'\n\
           \    * In the expression: h2 5\n\
           \      In an equation for `j2': j2 = h2 5\n\
           \(deferred type error)"#
    of co
    { __DEFAULT ->
    let {
      $d~ :: Int ~ Bool
      [LclId]
      $d~
        = Eq# @Type @Int @Bool @~(co :: Int ~# Bool) } in
    h2 $d~ (I# 5#)
    }

Notice the case statement on the typeError, instead of the let binding we saw in the previous example.

Richard suggested that we should make constraints unlifted (e.g. Constraint ~ TYPE (BoxedRep Unlifted) in Core), or, barring that, otherwise ensure that the evidence has been evaluated.

Note also that enabling -fdicts-strict does not make a difference to the issue reported here.

See also #11197 for the opposite issue (deferred type errors being evaluated too eagerly).