HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

Moduleghc-typelits-knownnat-0.7.12Haskell2010

GHC.TypeLits.KnownNat

Some "magic" classes and instances to get the GHC.TypeLits.KnownNat.Solver type checker plugin working.

Usage

Let's say you defined a closed type family Max:

import Data.Type.Bool (If)
import GHC.TypeLits

type family Max (a :: Nat) (b :: Nat) :: Nat where
  Max 0 b = b
  Max a b = If (a <=? b) b a

if you then want the GHC.TypeLits.KnownNat.Solver to solve KnownNat constraints over Max, given just KnownNat constraints for the arguments of Max, then you must define:

{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,
             MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,
             TypeApplications, TypeFamilies, TypeOperators,
             UndecidableInstances #-}

import Data.Proxy            (Proxy (..))
import GHC.TypeLits.KnownNat

instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where
  natSing2 = let x = natVal (Proxy a)
                 y = natVal (Proxy b)
                 z = max x y
             in  SNatKn z
  {-# INLINE natSing2 #-}

FAQ

1. GHC.TypeLits.KnownNat.Solver does not seem to find the corresponding KnownNat2 instance for my type-level operation

At the Core-level, GHCs internal mini-Haskell, type families that only have a single equation are treated like type synonyms.

For example, let's say we defined a closed type family Max:

import Data.Type.Bool (If)
import GHC.TypeLits

type family Max (a :: Nat) (b :: Nat) :: Nat where
  Max a b = If (a <=? b) b a

Now, a Haskell-level program might contain a constraint

KnownNat (Max a b)

, however, at the Core-level, this constraint is expanded to:

KnownNat (If (a <=? b) b a)

GHC.TypeLits.KnownNat.Solver never sees any reference to the Max type family, so it will not look for the corresponding KnownNat2 instance either. To fix this, ensure that your type-level operations always have at least two equations. For Max this means we have to redefine it as:

type family Max (a :: Nat) (b :: Nat) :: Nat where
  Max 0 b = b
  Max a b = If (a <=? b) b a
  • 3 types
  • 6 classes
  • 2 values
  • Cpp
  • MonoLocalBinds
  • TemplateHaskell
  • TemplateHaskellQuotes
  • ScopedTypeVariables
  • AllowAmbiguousTypes
  • TypeFamilies
  • GADTs
  • GADTSyntax
  • PolyKinds
  • DataKinds
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • MagicHash
  • KindSignatures
  • TypeOperators
  • ExplicitNamespaces
  • ExplicitForAll
  • TypeApplications

Singleton natural number

1 declaration

Constraint-level arithmetic classes

3 declarations
classclass KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where
#

Class for arithmetic functions with two arguments.

The Symbol f must correspond to the fully qualified name of the type-level operation. Use nameToSymbol to get the fully qualified TH Name as a Symbol

Methods

Instances6KnownNat2

Singleton boolean

2 declarations
valueboolVal :: KnownBool b => proxy b -> Bool
#

Get the Bool value associated with a type-level Bool

Use boolVal if you want to perform the standard boolean operations on the reified type-level Bool.

Use boolSing if you need a context in which the type-checker needs the type-level Bool to be either True or False

f :: forall proxy b r . KnownBool b => r
f = case boolSing @b of
  SFalse -> -- context with b ~ False
  STrue  -> -- context with b ~ True

KnownBool

1 declaration

Constraint-level boolean functions

newtypenewtype SBoolKb (f :: Symbol)
#

A type "representationally equal" to SBool, used for simpler implementation of constraint-level functions that need to create instances of KnownBool

Constructors

classclass KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where
#

Class for binary functions with a Boolean result.

The Symbol f must correspond to the fully qualified name of the type-level operation. Use nameToSymbol to get the fully qualified TH Name as a Symbol

Methods

Instances2KnownBoolNat2

Template Haskell helper

1 declaration