Dial the fancy even further back.

Author: robrix

semantic-analysis/src/Analysis/Syntax.hs

@@ -1,9 +1,4 @@
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
 module Analysis.Syntax
 ( -- * Syntax
   Term(..)
@@ -18,36 +13,30 @@ module Analysis.Syntax
 , Vec(..)
 ) where
 
-import           Control.Monad (guard)
-import           Data.Kind (Type)
+import           Data.Foldable (toList)
+import           Data.Functor.Classes
 import qualified Data.Set as Set
-import           Data.Typeable
-import           Unsafe.Coerce (unsafeCoerce)
 
 -- Syntax
 
 -- | (Currently) untyped term representations.
-data Term (sig :: Type -> Type) v where
+data Term sig v where
   Var  :: v -> Term sig v
-  (:$:) :: KnownNat n => sig n -> Vec n (Term sig v) -> Term sig v
+  (:$:) :: sig n -> Vec n (Term sig v) -> Term sig v
 
-instance (forall n . Eq (sig n), Eq v) => Eq (Term sig v) where
+instance (Eq1 sig, Eq v) => Eq (Term sig v) where
   Var v1   == Var v2   = v1 == v2
-  a :$: as == b :$: bs = case sameNat a b of
-    Just Refl -> a == b && as == bs
-    _         -> False
+  a :$: as == b :$: bs = liftEq (\ _ _ -> True) a b && toList as == toList bs
   _        == _        = False
 
-instance (forall n . Ord (sig n), Ord v) => Ord (Term sig v) where
+instance (Ord1 sig, Ord v) => Ord (Term sig v) where
   compare (Var v1)   (Var v2)   = compare v1 v2
   compare (Var _)    _          = LT
-  compare (a :$: as) (b :$: bs) = case sameNat a b of
-    Just Refl -> compare a b <> compare as bs
-    _         -> reifyNat a `compare` reifyNat b -- lol
+  compare (a :$: as) (b :$: bs) = liftCompare (\ _ _ -> EQ) a b <> compare (toList as) (toList bs)
   compare _          _          = GT
 
 
-subterms :: (forall n . Ord (sig n), Ord v) => Term sig v -> Set.Set (Term sig v)
+subterms :: (Ord1 sig, Ord v) => Term sig v -> Set.Set (Term sig v)
 subterms t = case t of
   Var _    -> Set.singleton t
   _ :$: ts -> Set.insert t (foldMap subterms ts)
@@ -64,22 +53,6 @@ type N2 = S N1
 type N3 = S N2
 
 
--- | Reify 'Nat's back from type-level singletons.
-class KnownNat n where
-  reifyNat :: proxy n -> Int
-
-instance KnownNat Z where
-  reifyNat _ = 0
-
-instance KnownNat n => KnownNat (S n) where
-  reifyNat _ = 1 + reifyNat (undefined :: proxy n)
-
-
--- | Test the equality of type-level 'Nat's at runtime, generating a type-level equality if equal.
-sameNat :: forall a b proxy1 proxy2 . (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
-sameNat a b = unsafeCoerce Refl <$ guard (reifyNat a == reifyNat b)
-
-
 -- FIXME: move this into its own module, or use a dependency, or something.
 data Vec n a where
   Nil :: Vec Z a