> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe