Equality in singletons for star kind

Question

I did in ghci:

> :set -XTypeOperators

> import Data.Proxy
> import Data.Type.Equality
> import Data.Singletons.Prelude

> :let p1 = Proxy :: Proxy (Int == Int)
> :let p2 = Proxy :: Proxy (Int :== Int)

> :t p1
p1 :: Proxy 'True
> :t p2
p2 :: Proxy (Int :== Int)

Why in the second case type is not calculated? Can I workaround it somehow? Can I make an instance for class PEq (where :== is defined)?

(ghc 7.10.3)

Update: I found how to make an instance. Are there some reasons why it is not included?

> instance PEq ('KProxy :: KProxy *) where { type (:==) x y = x == y }

or simple (as pointed by dfeuer in comments)

> instance PEq ('KProxy :: KProxy *)

or import this instance from TypeRepStar:

> import Data.Singletons.TypeRepStar()

You wouldn't even need the type definition; it defaults to exactly what you wrote. — dfeuer
It's intended and here's the explanation. It's clear from the extended discussion that a poly-kinded == is bad, but it's still not quite clear to me why the * instance isn't included by default. — András Kovács
@AndrásKovács Thanks for pointed that out. But the reason is unclear to me too. If I understand correct, user's instance for * could be implemented for requried set of types, not for all *-types. Probably with better performance? Is it really important here? — Dmitry Olshansky
@DmitryOlshansky since you found the answer, you should post it and accept it so this question doesn't remain unanswered. — sclv

Dmitry Olshansky Dmitry Olshansky · Accepted Answer · 2016-03-04T12:01:56

It seems that a reason for not including instance for PEq for kind * in singletons are similar to not including poly-kinded instances for Eq in base. It is described here. Such instance too common and if it exists we can't describe e.g. equalities of type arguments by result of type functions. For example:

Succ n == Succ m = n == m

For workaround in case of singletons one can define it:

instance PEq ('KProxy :: KProxy *)

Or just use it:

import Data.Singletons.TypeRepStar()

Equality in singletons for star kind

1 Answers