> On Jul 5, 2017, at 5:23 PM, Wolfgang Jeltsch <wolfgang...@jeltsch.info> 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.html#complete-user-supplied-kind-signatures-and-polymorphic-recursion). This surprised me, too, when I first encountered it, but I believe it's the correct behavior. Richard _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users