To Reduce or Not to Reduce

[fxdpntthm]

1. Elaboration should accompany reduction
2. Reduction is not always good.

• Top level definitions do not reduced eagerly (#25)
• Foreign Functions, Specialize pragmas, deriving context type signature reduce eagerly
  • [ ] Local bindings definitions should reduce eagerly. (let and where clause bindings)
  • [x] Specialize pragmas for instance declarations. (cf. in GHC.Base.Real {-# SPECIALIZE instance Enum Rational #-})

Cons: Wired in Desugaring passes need extra arguments making compilation fragile. Currently ill-typed core is compiled causing ghc-stage2 to produce a garbage binary.

[fxdpntthm]

One top level definition is problematic: runMainIO :: IO a -> IO a GHC internally generates a newbind for the logical main function typed at IO a

main :: IO a
main = ...

:Main.main :: IO a
:Main.main = runMainIO @a (main irr)

now if runMainIO's type is elaborated but not reduced, we get runMainIO :: IO @ a => IO a -> IO a

thus the binding generated for :Main.man is illtyped. it should ideally be :Main.main = runMainIO @a _ (main irr) now what should _ be? it should be of type IO @ a but that as we know is a unit constraint. but is a unit constraint inhabited by any literal? -- I don't know.

The definition of runMainIO is bunch of thread handling and top level exception handling that is obtained by interfacing foreign functions (rts).

There are 2 ways to solve this problem and producing a binary that doesn't crash.

1. don't elaborate the type of runMainIO
2. find a literal to inhabit (%%) a unit constraint

option 1 is easier; and it works.

[fxdpntthm]

similar problem with returnIO for evaluativing ghci statements This causes ghci to throw a PAP error.

[fxdpntthm]

The current solution: always reduce

• IO @ a
• [] @ a
• wft constraints for closed type families.

They will never cause problems unlike user defined datatypes as they are deeply wired in and we always know their RHS.