ghc-typelits-knownnat-0.7.5: Derive KnownNat constraints from other KnownNat constraints

GHC.TypeLits.KnownNat

Description

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,
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

Synopsis

# Singleton natural number

newtype SNatKn (f :: Symbol) Source #

Singleton natural number

Constructors

 SNatKn Natural

# Constraint-level arithmetic classes

class KnownNat1 (f :: Symbol) (a :: Nat) where Source #

Class for arithmetic functions with one argument.

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

class KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where Source #

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

#### Instances

Instances details
 (KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeNats.*" a b Source # KnownNat2 instance for GHC.TypeLits' * Instance detailsDefined in GHC.TypeLits.KnownNat MethodsnatSing2 :: SNatKn "GHC.TypeNats.*" Source # (KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeNats.+" a b Source # KnownNat2 instance for GHC.TypeLits' + Instance detailsDefined in GHC.TypeLits.KnownNat MethodsnatSing2 :: SNatKn "GHC.TypeNats.+" Source # (KnownNat a, KnownNat b, b <= a) => KnownNat2 "GHC.TypeNats.-" a b Source # KnownNat2 instance for GHC.TypeLits' - Instance detailsDefined in GHC.TypeLits.KnownNat MethodsnatSing2 :: SNatKn "GHC.TypeNats.-" Source # (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 "GHC.TypeNats.Div" x y Source # Instance detailsDefined in GHC.TypeLits.KnownNat MethodsnatSing2 :: SNatKn "GHC.TypeNats.Div" Source # (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 "GHC.TypeNats.Mod" x y Source # Instance detailsDefined in GHC.TypeLits.KnownNat MethodsnatSing2 :: SNatKn "GHC.TypeNats.Mod" Source # (KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeNats.^" a b Source # KnownNat2 instance for GHC.TypeLits' ^ Instance detailsDefined in GHC.TypeLits.KnownNat MethodsnatSing2 :: SNatKn "GHC.TypeNats.^" Source #

class KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where Source #

Class for arithmetic functions with three 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

# Singleton boolean

data SBool (b :: Bool) where Source #

Singleton version of Bool

Constructors

 SFalse :: SBool 'False STrue :: SBool 'True

boolVal :: forall b proxy. KnownBool b => proxy b -> Bool Source #

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

class KnownBool (b :: Bool) where Source #

Methods

#### Instances

Instances details
 Source # Instance detailsDefined in GHC.TypeLits.KnownNat Methods Source # Instance detailsDefined in GHC.TypeLits.KnownNat Methods

## Constraint-level boolean functions

newtype SBoolKb (f :: Symbol) Source #

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

Constructors

 SBoolKb Bool

class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k) where Source #

Class for ternary functions with a Natural 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

#### Instances

Instances details
 (KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool "Data.Type.Bool.If" a (b :: Nat) (c :: Nat) Source # Instance detailsDefined in GHC.TypeLits.KnownNat MethodsnatBoolSing3 :: SNatKn "Data.Type.Bool.If" Source #

class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k) where Source #

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

#### Instances

Instances details
 (KnownNat a, KnownNat b) => KnownBoolNat2 "GHC.TypeNats.<=?" (a :: Nat) (b :: Nat) Source # Instance detailsDefined in GHC.TypeLits.KnownNat MethodsboolNatSing2 :: SBoolKb "GHC.TypeNats.<=?" Source #

Convert a TH Name to a type-level Symbol