CODEWITHSUNDEEP
haskelltypeclasstype-level-computation
user1747134
user1747134

Reputation: 2472

Typeclass instance with arithmetic constraints on types

Basically, I would like to be able to do something like this:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
import GHC.TypeLits

newtype Foo (a::Nat) (b::Nat) c = Foo {getFoo :: c}

class Clz a where

instance Clz (Foo a (2*a) c) where

I.e., to make Foo a b instance of Clz only when a = 2*b.

I understand that the problem is in the (2*a) expression on the last line. When I try to compile it, I get:

• Illegal type synonym family application in instance:
    Foo a (2 * a) c
• In the instance declaration for ‘Clz (Foo a (2 * a) c)’

Is there a way to overcome this? How would I need to change the syntax? Do I need more language extensions? I am using latest GHC (8.0.1).

Upvotes: 1

Views: 109

Answers (1)

Tikhon Jelvis
Tikhon Jelvis

Reputation: 68152

You can use a type equivalence constraint (by enabling GADTs or type families):

instance (b ~ (2 * a)) => Clz (Foo a b c) where

This is a common technique for working with type families as seen in this other answer. That answer has a bit more explanation: this constraint doesn't mean exactly the same thing as the version you wanted, but will probably still work for your purposes.

Upvotes: 3

Related Questions