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

TP paratribulations at free.fr
Sat Sep 21 16:38:34 CEST 2013

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.


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 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 
      instance [overlap ok] ('Zero :< n) ~ 'True =>
                            Multiplication (Tensor n) Scalar (Tensor n)
        -- Defined at 
    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,


More information about the Haskell-Cafe mailing list