GitLab

Summary

GHC versions above 7.1 allow type equality constraints to prevent sharing.

Steps to reproduce

Compile the following without optimizations.

{-# language TypeFamilies #-}

module Main where

import Debug.Trace (trace)

myBool :: (a ~ Bool) => a
myBool = trace "expensive" False

value1 :: Bool
value1 = myBool

value2 :: Bool
value2 = myBool

main :: IO ()
main =
  value1 `seq`
  value2 `seq`
  return ()

Running yields the following output.

expensive
expensive

Expected behavior

The "expensive" myBool should be shared resulting in the following output.

expensive

GHC versions below 7.1 did not allow type equality coercions to prevent sharing as mentioned above and as I confirmed for the example above with GHC version 7.0.4. GHC's coercion representation was then changed in fdf86568 as described and motivated by the papers Equality proofs and deferred type errors, Evidence normalization in System FC, and Practical aspects of evidence-based compilation in System FC. Preventing sharing was not the author's motivation for the change. Indeed, the authors observed that "Programmers think of types as static objects, with zero run-time overhead, and they expect the same of proofs about types" and put some effort into convincing themselves that "the optimizer of GHC [...] can already eliminated the cost of equality proofs - except in corner cases where it would be wrong to do so." Did they simply overlook the consequences for sharing?

Environment

• GHC version used: 8.8.4