Hi TP, 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 Regards, Adam On Sat, Sep 21, 2013 at 10:38 AM, TP <paratribulati...@free.fr> wrote: > Hi everybody, > > I encouter some problem in my code in the following simple example: two > instances overlap for the multiplication sign `*`. The > `OverlappingInstances` extension is of no help because it seems GHC does not > look at the instance context to decide which instance is the most specific. > > file:///usr/share/doc/ghc-doc/html/users_guide/type-class- > extensions.html#instance-overlap > > How to make GHC realize that in the second instance below, the instance > context is not satisfied, such that the first instance has to be used? > (Indeed, a Scalar is a `Tensor 'Zero`, so the strict inequality `'Zero :< n` > is not satisfied in the context). > > -------------------------------------------- > {-# LANGUAGE DataKinds #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE StandaloneDeriving #-} > {-# LANGUAGE GADTs #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE FunctionalDependencies #-} > {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE OverlappingInstances #-} > > import Prelude hiding ((*)) > > data Nat = Zero | Succ Nat > deriving ( Show, Eq, Ord ) > > type family (m::Nat) :< (n::Nat) :: Bool -- Here Bool is a kind. > type instance m :< 'Zero = 'False > type instance 'Zero :< ('Succ n) = 'True > type instance ('Succ m) :< ('Succ n) = m :< n > > 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 (Tensor n) (Tensor n) where > s * t = Mult s t > > instance (('Zero :< n) ~ 'True) => > Multiplication (Tensor n) Scalar (Tensor n) where > t * s = Mult s t > > main = do > > let s = Tensor :: Scalar > let a = s*s > print a > -------------------------------------------- > > that yields at compilation: > > Overlapping instances for Multiplication > Scalar Scalar (Tensor 'Zero) > arising from a use of `*' > Matching instances: > instance [overlap ok] Multiplication Scalar (Tensor n) (Tensor n) > -- Defined at > test_overlapping_instance_with_typelevelinteger_test.hs:31:10 > instance [overlap ok] ('Zero :< n) ~ 'True => > Multiplication (Tensor n) Scalar (Tensor n) > -- Defined at > test_overlapping_instance_with_typelevelinteger_test.hs:34:10 > In the expression: s * s > In an equation for `a': a = s * s > In the expression: > do { let s = ...; > let a = s * s; > print a } > > > Thanks in advance, > > TP > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe