more type lit woe

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::Nat) <= (a::Nat), (b + d) ~  a) => AbsDiff a b d where  




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


{-#
*Data.TypeLits.GCD> :t a

<interactive>:1:1:
    Could not deduce (1 <= 2) arising from a use of `a'
    from the context (SingI Nat d, (1 + d) ~ 2)
      bound by the inferred type of
               it :: (SingI Nat d, (1 + d) ~ 2) => Sing Nat d
      at Top level
    Possible fix: add an instance declaration for (1 <= 2)
    In the expression: a
*Data.TypeLits.GCD> 

#-}