Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,324
    • Issues 4,324
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 373
    • Merge Requests 373
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #19238

Closed
Open
Opened Jan 19, 2021 by Sylvain Henry@hsyl20Developer

Recursive type families optimisation

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.
Edited Jan 19, 2021 by Sylvain Henry
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#19238