[Haskell-cafe] type-level integers, type-level operators, and most specific overlapping instance

[TP]

adam vogt wrote:

> You can add another instance to cover the case that everything is zero.
> Then you don't need the :<. Also it's convenient to arrange for the
> a,b,c to be the argument to Tensor, as given below:
> 
> class Multiplication a b c | a b -> c where
>     (*) :: Tensor a -> Tensor b -> Tensor c
> 
> instance Multiplication Zero Zero Zero where
>         s * t = Mult s t
> instance Multiplication Zero n n where
>         s * t = Mult s t
> instance Multiplication n Zero n where
>         t * s = Mult s t

Thanks a lot Adam. It is a pity I did not think to this solution myself. 
Below is the full code for a working version (however still using a more 
general definition of multiplication compared to yours).

But I have still a question: is the behavior of GHC correct in the example 
of my initial post? It is OK it does not look at the most specific instance 
by examining the instance context? Is it OK, or is it a deficiency?

Thanks,

TP

---------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Prelude hiding ((*))

data Nat = Zero | Succ Nat
    deriving ( Show, Eq, Ord )

data Tensor :: Nat -> * where
    Tensor :: Tensor order
    Mult   :: Scalar -> Tensor order -> Tensor order
deriving instance Show (Tensor order)

type Scalar = Tensor 'Zero

class Multiplication a b c | a b -> c where
    (*) :: a -> b -> c

instance Multiplication Scalar Scalar Scalar where
    s * s' = Mult s s'

instance Multiplication Scalar (Tensor n) (Tensor n) where
    s * t = Mult s t

instance Multiplication (Tensor n) Scalar (Tensor n) where
    t * s = Mult s t

main = do

let s = Tensor :: Scalar
let a = s*s
print a