type lit example problem 1

gistfile1.hs

{-# LANGUAGE DataKinds #-}              -- to declare the kinds
{-# LANGUAGE KindSignatures #-}         -- (used all over)
{-# LANGUAGE TypeFamilies #-}           -- for declaring operators + sing family
{-# LANGUAGE TypeOperators #-}          -- for declaring operator
{-# LANGUAGE EmptyDataDecls #-}         -- for declaring the kinds
{-# LANGUAGE GADTs #-}                  -- for examining type nats
{-# LANGUAGE PolyKinds #-}              -- for Sing family
{-# LANGUAGE UndecidableInstances #-}   -- for a bunch of the instances
{-# LANGUAGE FlexibleInstances #-}      -- for kind parameters
{-# LANGUAGE FlexibleContexts #-}       -- for kind parameters
{-# LANGUAGE ScopedTypeVariables #-}    -- for kind parameters\
{-# LANGUAGE MultiParamTypeClasses #-}  -- for <=, singRep, SingE
{-# LANGUAGE FunctionalDependencies #-} -- for SingRep and SingE




{-# OPTIONS_GHC -XNoImplicitPrelude #-}


    


module Data.TypeLits.GCD where

import GHC.TypeLits
--import GHC.Num(Integer, (-))


--class EqNat (a:: Nat) (b :: Nat) where 

--instance (SingI a, SingI b, a <= b, b<= a) =>  EqNat a b  where 


class AbsDiff (a::Nat) (b::Nat)  (d::Nat) | a b -> d where 

instance (SingI  a,SingI  b, SingI  d, (b + d) ~  a) => AbsDiff a b d where  




--this doesn't type check
a ::( AbsDiff 2 1 (d:: Nat ), SingI Nat, (1+d)~ 2)=> Sing d
a = sing 


{- Data/TypeLits/GCD.hs:44:5:
    Could not deduce (SingI Nat d) arising from a use of `sing'
    from the context (AbsDiff 2 1 d, SingI * Nat, (1 + d) ~ 2)
      bound by the type signature for
                 a :: (AbsDiff 2 1 d, SingI * Nat, (1 + d) ~ 2) => Sing Nat d
      at Data/TypeLits/GCD.hs:43:5-59
    Possible fix: add an instance declaration for (SingI Nat d)
    In the expression: sing
    In an equation for `a': a = sing
Failed, modules loaded: none. -}