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