shithub: MicroHs

Info  •  Files  •  Log  •  Branches

Make type equality polykinded

--- a/TODO

+++ b/TODO

@@ -41,5 +41,3 @@

 * Fix bug uncovered by Data.Type.Equality

 * mkQIdent

 * Do not use the C stack during evaluation

-* Fix bug:

-  foo :: forall e . Dict (Exception e) -> e -> String; foo d e = withDict d (displayException e)

--- a/lib/Data/Type/Equality.hs

+++ b/lib/Data/Type/Equality.hs

@@ -1,6 +1,7 @@

 module Data.Type.Equality(module Data.Type.Equality) where

 import Prelude

+type (:~:) :: forall k . k -> k -> Type

 data a :~: b = (a ~ b) => Refl

 instance forall a b . Eq (a :~: b) where

@@ -18,6 +19,5 @@

 castWith :: forall a b . (a :~: b) -> a -> b

 castWith Refl x = x

--- Problem: :~: is not polykinded

---apply :: forall (f :: Type -> Type) (g :: Type -> Type) a b . (f :~: g) -> (a :~: b) -> (f a :~: g b)

---apply Refl Refl = Refl

+apply :: forall f g a b . (f :~: g) -> (a :~: b) -> (f a :~: g b)

+apply Refl Refl = Refl

-- 

⑨