ref: 4bbd2e1708cb216e94efd7251ce18cff2bb04243
parent: 554f2c7b19b410d1203f7f278e6a35f5624ffee5
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Sun Nov 26 07:41:55 EST 2023
More bugs.
--- a/TODO
+++ b/TODO
@@ -46,12 +46,9 @@
* Fix polymorphic pattern literals
- Probably by implementing view patterns
* Make float support work for 32 and 64 bit words
-* Cache compiled modules:
- - Save the compilation cache at the end of each compilation.
- - On startup, read the cache. Validate each module by checking a checksum.
- - Keep a dependency graph with the cache for invalidation.
* Unicode, i.e., UTF-8 IO
* Use pointer reversal, might be slower
- In GC mark pass
- In evaluator
-* Make nullary type classes work.
+* Fix bug uncovered by Data.Type.Equality
+* Maybe allow implicit forall for kind variables?
--- /dev/null
+++ b/lib/Data/Type/Equality.hs
@@ -1,0 +1,25 @@
+module Data.Type.Equality(module Data.Type.Equality) where
+import Prelude
+
+data a :~: b = (a ~ b) => Refl
+
+-- BUG
+--instance forall a b . Eq (a :~: b) where
+-- Refl == Refl = True
+
+-- BUG
+--instance forall a b . Show (a :~: b) where
+-- show Refl = "Refl"
+
+sym :: forall a b . (a :~: b) -> (b :~: a)
+sym Refl = Refl
+
+trans :: forall a b c . (a :~: b) -> (b :~: c) -> (a :~: c)
+trans Refl Refl = Refl
+
+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
--
⑨