gistfile1.txt

% ghci -fplugin=GHC.TypeLits.Normalise
GHCi, version 8.4.3: http://www.haskell.org/ghc/  :? for help
Loaded package environment from /home/ogre/mess/nats/ghc-typelits-natnormalise-0.6.2/.ghc.environment.x86_64-linux-8.4.3
Loaded GHCi configuration from /home/ogre/.ghci
λ> :m +Ty
TyCoRep                 TyCon                   Type                    Type.Reflection         Type.Reflection.Unsafe  TysPrim                 TysWiredIn
λ> :m +Data.Type.Equality 
λ Data.Type.Equality> :m +GHC.TypeLits
λ D.T.Equality G.TypeLits> :set -XDataKinds 
λ D.T.Equality G.TypeLits> Refl :: 1 :~: 1

<interactive>:4:9: error:
    Illegal operator ‘:~:’ in type ‘1 :~: 1’
      Use TypeOperators to allow operators in types
λ D.T.Equality G.TypeLits> :set -XType
-XTypeApplications        -XTypeFamilies            -XTypeFamilyDependencies  -XTypeInType              -XTypeOperators           -XTypeSynonymInstances
λ D.T.Equality G.TypeLits> :set -XTypeOperators 
λ D.T.Equality G.TypeLits> Refl :: 1 :~: 1
Refl
λ D.T.Equality G.TypeLits> Refl :: forall n. n :~: n

<interactive>:7:17: error:
    Illegal symbol '.' in type
    Perhaps you intended to use RankNTypes or a similar language
    extension to enable explicit-forall syntax: forall <tvs>. <type>
λ D.T.Equality G.TypeLits> :set -XRankNTypes 
λ D.T.Equality G.TypeLits> Refl :: forall n. n :~: 1 + n

<interactive>:9:1: error:
    • Couldn't match type ‘n1’ with ‘1 + n1’
      ‘n1’ is a rigid type variable bound by
        an expression type signature:
          forall (n1 :: Nat). n1 :~: (1 + n1)
        at <interactive>:9:9-29
      Expected type: n1 :~: (1 + n1)
        Actual type: n1 :~: n1
    • In the expression: Refl :: forall n. n :~: 1 + n
      In an equation for ‘it’: it = Refl :: forall n. n :~: 1 + n
λ D.T.Equality G.TypeLits> Refl :: forall n. n + 1 :~: 1 + n
Refl