Copyright  (C) 2016 University of Twente 20172018 QBayLogic B.V. 2017 Google Inc. 

License  BSD2 (see the file LICENSE) 
Maintainer  Christiaan Baaij <christiaan.baaij@gmail.com> 
Safe Haskell  Trustworthy 
Language  Haskell2010 
Extensions 

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 (Proxya) y = natVal (Proxy
b) z = max x y inSNatKn
z {# INLINE natSing2 #}
FAQ
1. GHC.TypeLits.KnownNat.Solver does not seem to find the corresponding KnownNat2
instance for my typelevel operation
At the Corelevel, GHCs internal miniHaskell, 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 Haskelllevel program might contain a constraint
KnownNat (Max a b)
, however, at the Corelevel, 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 typelevel 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
Singleton natural number
Constraintlevel 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
typelevel operation. Use nameToSymbol
to get the fully qualified
TH Name as a Symbol
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
typelevel operation. Use nameToSymbol
to get the fully qualified
TH Name as a Symbol
Instances
(KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeNats.*" a b Source # 

Defined in GHC.TypeLits.KnownNat  
(KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeNats.+" a b Source # 

Defined in GHC.TypeLits.KnownNat  
(KnownNat a, KnownNat b, b <= a) => KnownNat2 "GHC.TypeNats." a b Source # 

Defined in GHC.TypeLits.KnownNat  
(KnownNat x, KnownNat y, 1 <= y) => KnownNat2 "GHC.TypeNats.Div" x y Source #  
Defined in GHC.TypeLits.KnownNat  
(KnownNat x, KnownNat y, 1 <= y) => KnownNat2 "GHC.TypeNats.Mod" x y Source #  
Defined in GHC.TypeLits.KnownNat  
(KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeNats.^" a b Source # 

Defined in GHC.TypeLits.KnownNat 
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
typelevel operation. Use nameToSymbol
to get the fully qualified
TH Name as a Symbol