[Haskell-cafe] writing a function to make a correspondance between type-level integers and value-level integers

[TP]

> I'm hoping that gets you moving again and seeing this helps you piece it
> all together.

Thanks a lot Richard,

It helped me a lot to move forward. No doubt your answer will be very useful 
for people looking for information on internet.

> - I changed the syntax of creating proxies. Instead of passing an
> argument, as you were trying, you set the type of a proxy using an
> explicit type annotation.

Indeed I did not realize that I could use `P::Proxy n`, and so that n does 
not need to be argument of the data constructor `P`. 

> - I added the extension ScopedTypeVariables, which allows method
> definitions to access type variables from an instance header.

In fact the extension ScopedTypeVariables is not needed to make your version 
work. However, if I extend a bit your version like that:

-------------
data Tensor :: Nat -> * where
    Tensor :: { order :: SNat order, name :: String } -> Tensor order

instance MkSNat o => Show (Tensor o) where
    show Tensor { order = o, name = str } = str ++ " of order "
            ++ (show (mkSNat (P :: Proxy o)))  --- (*1*)
--------------

and in the "main" part:

--------------
let vector = Tensor { order = mkSNat (P::Proxy order), name = "u" } :: 
Tensor (Succ Zero)
print vector
---------------

then the line (*1*) makes mandatory to use the extension 
ScopedTypeVariables. But I don't see the difference with your line:

---------------
instance MkSNat n => MkSNat ('Succ n) where
   mkSNat _ = SSucc (mkSNat (P :: Proxy n))
---------------

So I don't understand why ScopedTypeVariables is needed in one case and not 
in the other.

> - I added an extra constraint to the Succ instance for MkSNat, requiring
> that n is in the MkSNat class, as well.

I understand why we are compelled to use a constraint here:

---------------
instance MkSNat n => MkSNat ('Succ n) where
   mkSNat _ = SSucc (mkSNat (P :: Proxy n))
---------------

My understanding is that we are compelled to put a constraint `MkSNat n` 
because we cannot be sure that n (which is a type of kind Nat because type 
constructor Succ takes a type of kind Nat as argument to make a concrete 
type) is an instance of MkSNat because we are precisely defining this 
instance.

However, why am I compelled to put a constraint in 

---------------
instance MkSNat o => Show (Tensor o) where
    show Tensor { order = o, name = str } = str ++ " of order "
            ++ (show (mkSNat (P :: Proxy o)))  --- (*1*)
---------------
?
Indeed, we know that Tensor takes a type of kind Nat to make a concrete 
type, so o is a type of kind Nat. And we have made `'Succ n` and `Zero` 
instances of MkSNat; are we compelled to put a constraint because Haskell 
makes the hypothesis that o could be another type of kind Nat different from 
`'Succ n` and `Zero`? If yes, is it related to the sentence I have already 
read: "Typeclasses are open"?

Thanks,

TP