Add colorable and decorable.

[haskell/symantic.git] / symantic / Language / Symantic / Typing / Unify.hs

diff --git a/symantic/Language/Symantic/Typing/Unify.hs b/symantic/Language/Symantic/Typing/Unify.hs
index 67d34fdb5139ccfb8b7bc3c52cfd0320761fdc9c..c0709df4d36902bde818bebe67b15a153b770e8c 100644 (file)
--- a/symantic/Language/Symantic/Typing/Unify.hs
+++ b/symantic/Language/Symantic/Typing/Unify.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Language.Symantic.Typing.Unify where
 
@@ -131,10 +130,10 @@ data Error_Unify src
 deriving instance Source src => Eq   (Error_Unify src)
 deriving instance Source src => Show (Error_Unify src)
 
-instance Inj_Error (Error_Unify src) (Error_Unify src) where
-       inj_Error = id
-instance Inj_Error (Con_Kind src) (Error_Unify src) where
-       inj_Error = Error_Unify_Kind
+instance ErrorInj (Error_Unify src) (Error_Unify src) where
+       errorInj = id
+instance ErrorInj (Con_Kind src) (Error_Unify src) where
+       errorInj = Error_Unify_Kind
 
 -- | Return the left spine of a 'Type':
 -- the root 'Type' and its 'Type' parameters,
@@ -142,17 +141,17 @@ instance Inj_Error (Con_Kind src) (Error_Unify src) where
 spineTy ::
  forall src vs t.
  Source src =>
- Inj_Source (TypeVT src) src =>
+ SourceInj (TypeVT src) src =>
  Type src vs t ->
  (TypeT src vs, [TypeT src vs])
 spineTy typ = go [] typ
        where
-       go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
+       go :: forall kx (x::kx). [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
        go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
         | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
         = go ctx t -- NOTE: skip the constraint @q@.
-       go ctx (TyApp  _src f a) = go (TypeT (a `source` TypeVT typ) : ctx) f
-       go ctx t = (TypeT (t `source` TypeVT typ), ctx)
+       go ctx (TyApp  _src f a) = go (TypeT (a `withSource` TypeVT typ) : ctx) f
+       go ctx t = (TypeT (t `withSource` TypeVT typ), ctx)
 
 {-
 spineTy
@@ -174,8 +173,8 @@ spineTy = go TypesZ
 -- | Return the /most general unification/ of two 'Type's, when it exists.
 unifyType ::
  forall ki (x::ki) (y::ki) vs src.
- Inj_Source (TypeVT src) src =>
- Inj_Error (Con_Kind src) (Error_Unify src) =>
+ SourceInj (TypeVT src) src =>
+ ErrorInj (Con_Kind src) (Error_Unify src) =>
  Subst src vs ->
  Type src vs (x::ki) ->
  Type src vs (y::ki) ->