CODEWITHSUNDEEP
haskelltype-familiesdata-kinds
Dmitry Olshansky
Dmitry Olshansky

Reputation: 483

Why compiler couldn't match type 'a==a' with '`True' for type family?

Is there some reason why this code is not compiled:

type family Foo a b :: Bool where
    Foo a b = a == b

foo :: Foo a b ~ True => Proxy a -> Proxy b
foo _ = Proxy

bar :: Proxy a -> Proxy a
bar = foo

with error:

Couldn't match type ‘a == a’ with ‘'True’
Expected type: 'True
  Actual type: Foo a a

but if I change type family definition to

type family Foo a b :: Bool where
    Foo a a = True
    Foo a b = False

it is compiled well?

(ghc-7.10.3)

Upvotes: 8

Views: 211

Answers (1)

Dmitry Olshansky
Dmitry Olshansky

Reputation: 483

Due to a request for a complete working example from Daniel Wagner, I found an answer.

Complete example at first:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
module Test where

import Data.Type.Equality(type (==))
import Data.Proxy(Proxy(..))

type family Foo a b :: Bool where
    Foo a b = a == b

foo :: Foo a b ~ True => Proxy a -> Proxy b
foo _ = Proxy

bar :: Proxy a -> Proxy a
bar = foo

The problem here is with PolyKinds pragma. Without it it works well. I probably need it so that I can write

bar :: Proxy (a :: *) -> Proxy a

and all goes well.

The reason is clear now. The type family (==) has no poly-kinded instances (details explaining why such instances aren't provided here) so we can't reduce all equalities. So we need to specify a kind.

Upvotes: 9

Related Questions