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

Question

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)

Luxuriant

Where is the type family == defined? Is it lifted from instances automatically by GHC? If so, GHC has to account for the possibility of a weird instance where on some custom type (==) = \_ _ -> False, I guess. – Dieterich

Can you include a complete working example? When I try your example, I get different errors than the one you showed. – Copilot

@chi, or not weird: (let x = 0/0 in x == x) ~> False. – Jeffreyjeffreys

Answer 1

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.

Luxuriant

@haoformayor When quoting content from outside sources you should use blockquotes, so that it's clear what was quoted. In this specific case the formatting was terrible and would require some treatment. Also the content you edited in is not essential to answer the question and as such there's no need to actually copy it. The answer is already complete without it, the "why" no polykinded instance is provided can be answered in an other question or just left as a link for further reading. – Flori

What is the utility of your == type family? It's usually much easier to work with native type equality (~) than it is to build a Boolean equality into the type system. At the end of the day you have to use ~ to do anything with the result of ==, as you did in foo. – Blaspheme

@BenjaminHodgson: == is not mine. It is from the base package. It is a type family which result has kind Bool. On the other hand, result of ~ has kind Constraint. So == is usable in boolean type level calculation. You can't use ~ instead there. – Luxuriant

My question is really why are you using Boolean equality and not propositional equality? – Blaspheme

@BenjaminHodgson propositional equality (:~:) is a data type with kind *. I can't see how to use it instead of type family == in type calculation. It seems too common question about all these equalities for comments. Probably better to ask it separately? – Luxuriant