Version 91 (modified by simonpj, 3 years ago) (diff)


Type Functions, Type Families, and Associated Types in GHC - The Master Plan

This page serves as a collection of notes concerning the implementation of type families (aka type functions) and associated types, especially about the implications for type checking, interface files, and FC intermediate code generation.

See the Haskell Wiki for user-level documentation.


Detailed information about implemented and unimplemented features as well as bugs and plans for further improvements is at implementation status. The following provides a summary:

Implemented features:

  • All basic functionality of open data type families, open type synonym families, and equality constraints has been implemented.
  • Type checking is fully integrated with GADTs.
  • Type family instances can have ordered groups of equations. See NewAxioms.

Missing features:

  • Superclass equalities.
  • Data family instances in GADT form.
  • Re-implement functional dependencies using explicit equalities.

Speculative ideas:

  • Total type families.
  • Closed synonym families.
  • Class families.
  • Our type-indexed data types are open. However, we currently don't allow case expressions mixing constructors from different indexes. We could do that if we had a story for open function definitions outside of classes. Class instances of entire data families (including deriving clauses at family declarations to derive for all instances) requires the same sort of capabilities as case expressions mixing data constructors from different indexes. This is, as they require to build a dictionary that applies to all family instances (as opposed to a distinct dictionary per instance, which is what we have now).


Use Keyword = TypeFamilies to ensure that a ticket ends up on these lists.

Open Tickets:

Relax restrictions on type family instance overlap
Improve consistency checking for family instances
Type family instance overlap accepted in ghci
data families and TH names do not mix well (e.g. cannot use TH deriving)
TypeFamilies painfully slow
Type family patterns should support as-patterns.
Roles for type families
Less conservative compatibility check for closed type families
Allow family instances in an hs-boot file
Type families returning quantified types
More informative error messages when closed type families fail to simplify
Show data/type family instances with ghci's :info command
Alternative to type family Any
Type families + hs-boot files = unsafeCoerce
Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.
Programs that require AllowAmbiguousTypes in 7.8
Type inference is weaker for GADT than analogous Data Family
dep_orphs in Dependencies redundantly records type family orphans
Wanted: higher-order type-level programming
GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family
Closed type families: Warn if it doesn't handle all cases
CUSK mysteries
Odd interaction between rank-2 types and type families
Devise workaround for how infinite types prevent closed type family reduction
Not enough unboxing happens on data-family function argument
Notify user when a kind mismatch holds up a type family reduction
Odd interaction between record update and type families
Generalize injective type families
Use injective type families (decomposition) when dealing with givens
family is treated as keyword in types even without TypeFamilies enabled
Type-level arithmetic of sized-types has weaker inference power than in 7.8
Some type families don't reduce with :kind!
Type family If is too strict
GHC cannot infer injectivity on type family operating on GHC.TypeLits' Nat, but can for equivalent type family operating on user-defined Nat kind
Flag to not expand type families
Surprising accepted constructor for GADT instance of data family
"Occurs check" not considered when reducing closed type families
Type family producing infinite type accepted as injective
Allow class associated types to reference functional dependencies
Make type indices take local constraints into account in type instance declaration
Type family in type pattern kind
Ambiguity Caused By PolyKind and Not Helpful Error Messages
Must perform family consistency check on non-imported identifiers
Poor compiler performance with type families
Injective type family syntax accepted without TypeFamilyDependencies
Misleading "Kind mis-match on LHS of default declaration" error
Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
strange error when using data families with levity polymorphism and unboxed sums and data families
Type families interfere with specialisation rewrite rules
Stuck type families can lead to lousy error messages
Data families should not instantiate to non-Type kinds
Allow type family in data family return kind
Display coaxiom branch incompatibilities in GHCi
Reduce type families in equations' RHS when testing equation compatibility
TypeInType: Type error conditioned on ordering of GADT and type family definitions
Error message involving type families points to wrong location
coerce fails for Coercible type families
Discrepancy between seemingly equivalent type synonym and type family
Data familes should end in Type
Better inferred signatures
Clean up family instance consistency checking

Closed Tickets:

Newtype deriving doesn't work with type families
UNPACK doesn't unbox data families
TypeFamilies don't seem to play with LIberalTypeSynonyms
Injective type families
Kind-indexed type family failure with polymorphic kinds
Regression error: Kind variables don't work inside of kind constructors in type families
GHC 7.4.2 crashes with a panic when using type families and data kinds together
Kind variable problem when declaring associated type family
"Pattern match on GADT" error for non-GADT
Failure to let kind variable remain uninstantiated when not needed
type inference fails with where clause (RankNTypes, TypeFamilies)
reifyInstances can't deal with polykinded type families
Panic in conflictInstErr when branched type family instances conflict
Core lint failure when optimizing coercions in branched axioms
Use GeneralizedNewtypeDeriving to automatically create associated type families
either bug or confusing error message mixing PolyKinds and TypeFamilies
Associated Type Synonyms do not unfold in InstanceSigs
Odd failure to deduce a constraint
Type families + hs-boot files = panic (type family consistency check too early)
Error warns about non-injectivity of injective type family
Local open type families instances ignored during type checking
Regression when deriving Generic1 on poly-kinded data family
Type aliases twice as slow to compile as closed type families.
Put injective type families in a separate language extension
* is not an indexed type family
-XTypeInType uses up all memory when used in data family instance
Typechecker hangs when checking type families with -ddump-tc-trace turned on
TypeFamilyDependencies on Data.Type.Bool's `Not`
:kind command allows unsaturated type family,
Type families, `TypeError`, and `-fdefer-type-errors` cause "opt_univ fell into a hole"
Can't create injective type family equation with TypeError as the RHS
GHC is oblivious to injectivity when solving an equality constraint
Dependent type family does not reduce
GHC panic when resolving Show instance
Type family reduction irregularity (change from 7.10.3 to 8.0.1)
Associated type family instance validity checking is too conservative
Bizarre pretty-printing of closed type families in GHCi
Singletons code fails to typecheck when type signature involving type family is added
GHC doesn't reduce type family in kind signature unless its arm is twisted
TH-reified type family and data family instances have a paucity of kinds
Lift the "Illegal polymorphic type" restriction on type families
Can't apply higher-ranked kind in type family
GHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instance
GHCi allows unsaturated type family
GHC 8.2 error message around indexes for associated type instances is baffling
GHC 8.0 regression: ‘k’ is not in scope during type checking, but it passed the renamer
Out of scope errors with type families do not mention scope
Datatypes cannot use a type family in their return kind
Data family instances must list all patterns of family, despite documentation's claims to the contrary
Difference between newtype and newtype instance
"Conflicting family instance" error pretty prints data family instances poorly
GHC-inferred type signature doesn't actually typecheck
GHC doesn't use the fact that Coercible is symmetric
Type family equation refuses to unify wildcard type patterns
Duplicate type family instances are permitted
GHC HEAD regression involving type families in kinds
deriving on associated data types fails to find constraints
Wrong warning by -Wincomplete-patterns
Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F
Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?
Pattern matching on GADT does not refine type family parameters
GHC HEAD regression involving TYPEs in type families
Lint types created by newFamInst
GHC HEAD regression: tcTyVarDetails
Type inference regression between GHC 8.0.2 and 8.2.2
Core Lint error involving newtype family instances with wrappers
:info prints kinds in closed type family equations without enabling -fprint-explicit-kinds
Infinite typechecker loop in GHC 8.6
Oversaturated type family application panicks GHC (piResultTys2)
Bogus "No instance" error when type families appear in kinds
Kind variables in type family aren't quantified in toposorted order
Inconsistent kind variable binder visibility between associated and non-associated type families
Type families without CUSKs cannot be given visible kind variable binders
Marking Pred(S n) = n as injective
Different saturations of the same polymorphic-kinded type constructor aren't seen as apart types
Type family with higher-rank result is too accepting
Core Lint error with invalid newtype declaration
Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times)
Type family equation foralls allow strange re-quantification of class-bound type variables
Bad axiom produced for polykinded data family
Poor error message source location reporting with unsaturated type family
Type family equation with wrong name is silently accepted (GHC 8.6+ only)
GHC HEAD type family regression involving invisible arguments


Data-type family: a data type declared with a data family declaration.

Type-synonym family, or type function: a type synonym declared with a type family declaration.

Type family: a data-type family or type-synonym family.

Parametric type constructors: the type constructor of a vanilla Haskell type.

Family type constructor or Family TyCon: the type constructor for a type family.

Instance TyCon: the TyCon arising from a data/newtype/type instance declaration. Sometimes called the representation TyCon. The instance TyCon is invisible to the programmer; it is only used internally inside GHC.

Associated type: A type family that is declared in a type class.

Kind signature: Declaration of the name, kind, and arity of an indexed type constructor. The arity is the number of type indexes - not the overall number of parameters - of an indexed type constructor.

Definitions vs. declarations: We sometimes call the kind signature of an indexed constructor its declaration and the subsequent population of the type family by type equations or indexed data/newtype declarations the constructor's definition.

Note: we previously used the term "indexed type", but have now switched to using "type family". Please change any uses of the former into the latter as you come across them.

How It Works

The details of the implementation are split over a couple of subpages, due to the amount of the material:

Furthermore, we have


  • Type Checking with Open Type Functions. Tom Schrijvers, Simon Peyton-Jones, Manuel M. T. Chakravarty, and Martin Sulzmann. In Proceedings of ICFP 2008 : The 13th ACM SIGPLAN International Conference on Functional Programming, ACM Press, pages 51-62, 2008.
  • Associated Types with Class. Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, and Simon Marlow. In Proceedings of The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), ACM Press, pages 1-13, 2005.
  • Associated Type Synonyms. Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. In Proceedings of The Tenth ACM SIGPLAN International Conference on Functional Programming, ACM Press, pages 241-253, 2005.
  • Towards Open Type Functions for Haskell. Tom Schrijvers, Martin Sulzmann, Simon Peyton-Jones, and Manuel M. T. Chakravarty. Presented at IFL 2007.
  • Type Checking with Open Type Functions. Tom Schrijvers, Simon Peyton-Jones, Manuel M. T. Chakravarty, and Martin Sulzmann. ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming, ACM Press, 2008.
  • Old and outdated wiki material on type checking with indexed synonyms.