[Haskell-cafe] Equality test between types that returns type-level Bool ?

[Takayuki Muranushi]

Is it possible to write

type family SameType a b :: Bool

which returns True if a and b are the same type, and False otherwise?

I encountered this problem when I was practicing promoted lists and
tuples in ghc-7.6.1. One of my goal for practice is to write more
"modular" version of extensible-dimensional calculations, and to
understand whether ghc-7.6.1 is capable of it.

http://hackage.haskell.org/packages/archive/dimensional/0.10.2/doc/html/Numeric-Units-Dimensional-Extensible.html

Some of my attempts:

https://github.com/nushio3/dimensional-tf/blob/master/attic/list-02.hs
This fails because :==: is not an equality test between a and b, but
is a equality test within a (promoted) kind.

https://github.com/nushio3/dimensional-tf/blob/master/attic/list-03.hs
This fails because type instance declarations are not read from top to
bottom. (not like function declarations.)

https://github.com/nushio3/dimensional-tf/blob/master/attic/map-03.hs
I could define a lookup using class constraints, but when I use it,
results in overlapping instances.

So, will somebody teach me which of the following is correct?

* We can write a type family SameType a b :: Bool
* We cannot do that because of theoretical reason (that leads to
non-termination etc.)
* We cannot write SameType, but there are ways to write functions like
'filter' and 'merge' , over type-level lists, without using SameType.

Always grateful to your help,
--
Takayuki MURANUSHI
The Hakubi Center for Advanced Research, Kyoto University
http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html