Re: Heterogeneous equality

On Jul 5, 2017, at 5:23 PM, Wolfgang Jeltsch wrote:

Hi!

The base package contains the module Data.Type.Equality, which contains the type (:~:) for homogeneous equality. I was a bit surprised that there is no type for heterogeneous equality there. Is there such a type somewhere else in the standard library?

I don't believe it is, but (in my opinion) it should be.

I tried to define a type for heterogeneous equality myself as follows:

...

{-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}

data a :~~: b where

HRefl :: a :~~: a

To my surprise, the kind of (:~~:) defined this way is k -> k -> *, not k -> l -> *. Why is this?

Because the definition of heterogeneous equality requires polymorphic recursion, in that the usage of (:~~:) in the type of HRefl has different kind indices than the declaration head. Polymorphic recursion is allowed only when you have a *complete user-supplied kind signature*, as documented here (https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...). This surprised me, too, when I first encountered it, but I believe it's the correct behavior. Richard