GitLab

Motivation

Consider the following simple example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Foo where

import GHC.TypeNats

type family Index n xs where
    Index 0 (x:_)  = x
    Index n (_:xs) = Index (n-1) xs


x :: Index 2 '[Float,Int,Bool]
x = True

It results in a lot of bloat in Core:

-- RHS size: {terms: 1, types: 0, coercions: 56, joins: 0/0}
x :: Index 2 '[Float, Int, Bool]
[GblId,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
         Tmpl= GHC.Types.True
               `cast` (Sub (Sym (Foo.D:R:Index[0] <Bool>_N <'[]>_N))
                       ; (Index (Sym (SubDef (<1>_N, <1>_N))) <'[Bool]>_N)_R
                       ; Sub (Sym (Foo.D:R:Index[1] <1>_N <Int>_N <'[Bool]>_N))
                       ; (Index (Sym (SubDef (<2>_N, <1>_N))) <'[Int, Bool]>_N)_R
                       ; Sub (Sym (Foo.D:R:Index[1] <2>_N <Float>_N <'[Int, Bool]>_N))
                       :: Bool ~R# Index 2 '[Float, Int, Bool])}]
x = GHC.Types.True
    `cast` (Sub (Sym (Foo.D:R:Index[0] <Bool>_N <'[]>_N))
            ; (Index (Sym (SubDef (<1>_N, <1>_N))) <'[Bool]>_N)_R
            ; Sub (Sym (Foo.D:R:Index[1] <1>_N <Int>_N <'[Bool]>_N))
            ; (Index (Sym (SubDef (<2>_N, <1>_N))) <'[Int, Bool]>_N)_R
            ; Sub (Sym (Foo.D:R:Index[1] <2>_N <Float>_N <'[Int, Bool]>_N))
            :: Bool ~R# Index 2 '[Float, Int, Bool])

The number of coercions balloons quickly:

Type	# coercions
Index 1 '[Float,Bool]	28
Index 2 '[Float,Char,Bool]	56
Index 3 '[Float,Char,Int,Bool]	90
Index 4 '[Float,Char,Int,String,Bool]	134

Now if we also define y = x we get:

-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
y :: Bool
[GblId,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
         Tmpl= GHC.Types.True}]
y = GHC.Types.True

GHC has dropped the coercion!

Proposal

1. Ideally x should be automatically rewritten exactly as y (i.e., coercions should be dropped when possible).
2. We could perhaps avoid role conversions on every Coercion (e.g. by doing the whole chain of TransCo nominally and then only Subing at the end)
3. Perhaps add Sym as a boolean field of common coercions and axioms (FunCo, SubDef, etc.) to avoid an indirection
4. Coercions are currently LCF-like proofs. It could be worth trying to store them as tactics instead: for example replacing the chain of instantiated type family application coercions (e.g. Index (Sym (SubDef (<2>_N, <1>_N))) <'[Int, Bool]>_N) with a more generic Reduce with Index n times on the RHS.