## Could not deduce KnownNat in two existentials with respect to the singletons library

Question

I was experimenting with the singletons library and I found a case that I don't understand.

``````{-# LANGUAGE GADTs, StandaloneDeriving, RankNTypes, ScopedTypeVariables,
FlexibleInstances, KindSignatures, DataKinds, StandaloneDeriving  #-}

import Data.Singletons.Prelude
import Data.Singletons.TypeLits

data Foo (a :: Nat) where
Foo :: Foo a
deriving Show

data Thing where
Thing :: KnownNat a => Foo a -> Thing

deriving instance Show Thing

afoo1 :: Foo 1
afoo1 = Foo

afoo2 :: Foo 2
afoo2 = Foo

athing :: Thing
athing = Thing afoo1

foolen :: forall n. KnownNat n => Foo n -> Integer
foolen foo =
case sing of (SNat :: Sing n) -> natVal (Proxy :: Proxy n)

minfoo :: forall a b c. (Min a b ~ c, KnownNat c) => Foo a -> Foo b -> Integer
minfoo _ _ =
let c = case sing of (SNat :: Sing c) -> natVal (Proxy :: Proxy c)
in natVal (Proxy :: Proxy c)

thinglen :: Thing -> Integer
thinglen (Thing foo) = foolen foo
``````

I could use this to get the minimum of two Things

``````minthing :: Thing -> Thing -> Integer
minthing (Thing foo1) (Thing foo2) = min (foolen foo1) (foolen foo2)
``````

But why can't I just do this?

``````minthing' :: Thing -> Thing -> Integer
minthing' (Thing foo1) (Thing foo2) = minfoo foo1 foo2

• Could not deduce (KnownNat
(Data.Singletons.Prelude.Ord.Case_1627967386
a
a1
(Data.Singletons.Prelude.Ord.Case_1627967254
a a1 (GHC.TypeLits.CmpNat a a1))))
``````

Show source

## Answers to Could not deduce KnownNat in two existentials with respect to the singletons library ( 1 )

1. You need to do some theorem proving to check that given `KnownNat a` and `KnownNat b` you can get `KnownNat (Min a b)`. A possible solution:

``````import Data.Constraint
``````

(...)

``````theorem :: forall a b. (KnownNat a, KnownNat b) =>
Sing a -> Sing b -> Dict (KnownNat (Min a b))
theorem sa sb = case sCompare sa sb of
SLT -> Dict
SEQ -> Dict
SGT -> Dict

fooSing :: forall a. KnownNat a => Foo a -> Sing a
fooSing _ = sing

minthing' :: Thing -> Thing -> Integer
minthing' (Thing foo1) (Thing foo2) =
case theorem (fooSing foo1) (fooSing foo2) of
Dict -> minfoo foo1 foo2
``````