type level constraint encoding-CodePudding

So I have a data constructor that I only use at the type level which contains a Nat. Normally if I pass this around at the type level and I want to reflect the Nat to the term level I need a KnownNat constraint. What I want to do is encode this KnownNat constraint into the type itself so if this type occurs in a signature somewhere a KnownNat constraint is inferred in the body of the function. This means I would no longer need to write the KnownNat constraint at usage sites. I only need to make sure the KnownNat constraint is met at construction.

I thought to use GADT for this and got this far:

data Foo = Foo Nat Nat

type family GetA (f :: Foo) :: Nat where
  GetA ('Foo a _) = a

type family GetB (f :: Foo) :: Nat where
  GetB ('Foo _ b) = b

data KnownFoo (f :: Foo) where
  KnownFoo :: (KnownNat (GetA f), KnownNat (GetB f)) => KnownFoo f

foo :: forall (f :: Foo) (kf :: KnownFoo f). Proxy kf -> Integer
foo _ = natVal $ Proxy @(GetA f)

But this doesn't work as the type checker doesn't understand that GetA f is a KnownNat even though a KnownFoo is passed in. Is there a way to make something like this work?

I also tried to move the f :: Foo entirely into the KnownFoo constraint like so:

data Foo = Foo Nat Nat

type family GetA (f :: Foo) :: Nat where
  GetA ('Foo a _) = a

type family GetB (f :: Foo) :: Nat where
  GetB ('Foo _ b) = b

data KnownFoo where
  KnownFoo :: forall f. (KnownNat (GetA f), KnownNat (GetB f)) => Proxy f -> KnownFoo

type family GetFoo (kf :: KnownFoo) :: Foo where
  GetFoo ('KnownFoo (Proxy f)) = f

But then I have no way to write the GetFoo type family since it complains that KnownNat is unpromotable.

Any help is appreciated!

CodePudding user response：

I'm not sure I fully understand what you need, but if you want to store a KnownNat constraint, you'll have to have some runtime representation of that. Perhaps something like this may work for you:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

import GHC.TypeLits

data FooC a b where
    FooR :: (KnownNat a, KnownNat b) => FooC a b

type family GetA x where GetA (FooC a b) = a
type family GetB x where GetB (FooC a b) = b

withKnowledge :: FooC a b -> ((KnownNat a, KnownNat b) => r) -> r
withKnowledge FooR r = r

Note that DataKinds is not even on here: we are directly defining the new type we want rather than indirectly defining a lowered form of it. You can make a similar Known class for this, I guess.

class KnownFoo f where witness :: f
instance (KnownNat a, KnownNat b) => KnownFoo (FooC a b) where witness = FooR

withKnownFoo :: forall f a b r. (KnownFoo f, f ~ FooC a b) => ((KnownNat (GetA f), KnownNat (GetB f)) => r) -> r
withKnownFoo = withKnowledge (witness @f)

It doesn't seem super useful, though. Any time you could write withKnownFoo x, you already have the appropriate KnownNat instances in scope to just write x and have its constraints met anyway.