Skip to content

Make unit types coercible

Motivation

Unit types, i.e. types with exactly one constructor with no parameters obviously are isomorphic to (), so they should be coercible. Yet, this code does not typecheck

module Tmp where
import Data.Coerce

data Unit1 = Unit1 deriving Show
data Unit2 = Unit2 deriving Show

test = (coerce Unit1) :: Unit2

===

tmp.hs:7:9: error:
    • Couldn't match representation of type ‘Unit1’
                               with that of ‘Unit2’
        arising from a use of ‘coerce’
    • In the expression: (coerce Unit1) :: Unit2
      In an equation for ‘test’: test = (coerce Unit1) :: Unit2
  |
7 | test = (coerce Unit1) :: Unit2

Realistically, this isn't a big issues on its own as coercion of newtypes is rarely needed. However, it is illogical and might be an issue in code, dealing with singletons-as-proofs.

Proposal

make compiler provide instances of Coercible for all unit type pairs.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information