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!
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.