symantic/Language/Symantic/Typing/Unify.hs

   1 {-# LANGUAGE ExistentialQuantification #-}
   2 {-# LANGUAGE TypeInType #-}
   3 {-# LANGUAGE UndecidableInstances #-}
   4 {-# LANGUAGE ViewPatterns #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6 module Language.Symantic.Typing.Unify where
   7
   8 import Data.Map.Strict (Map)
   9 import Data.Semigroup (Semigroup(..))
  10 import Unsafe.Coerce (unsafeCoerce)
  11 import qualified Data.Map.Strict as Map
  12
  13 import Language.Symantic.Grammar
  14 import Language.Symantic.Typing.Variable
  15 import Language.Symantic.Typing.Kind
  16 import Language.Symantic.Typing.Type
  17 import Language.Symantic.Typing.Show ()
  18
  19 -- * Type 'Subst'
  20 -- | /Type variable substitution/.
  21 --
  22 -- WARNING: a 'Subst' MUST be without loops, and fully expanded.
  23 newtype Subst src vs
  24  =      Subst (Map IndexVar (VT src vs))
  25 deriving instance Source src => Show (Subst src vs)
  26 instance Semigroup (Subst src vs) where
  27         (<>) = unionSubst
  28 instance Monoid (Subst src vs) where
  29         mempty  = Subst Map.empty
  30         mappend = (<>)
  31
  32 -- | Unify two 'Subst's.
  33 --
  34 -- NOTE: the union is left-biased: in case of duplicate 'Var's,
  35 -- it keeps the one from the first 'Subst' given.
  36 --
  37 -- NOTE: the first 'Subst' given is applied to the second (with 'subst'),
  38 -- this way each 'Var' directly maps to an expanded 'Type',
  39 -- so that, when using the resulting 'Subst',
  40 -- there is no need to apply it multiple times
  41 -- until there is no more substitution to be done.
  42 unionSubst :: Subst src vs -> Subst src vs -> Subst src vs
  43 unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) <$> y)
  44
  45 -- * Type 'VT'
  46 -- | A 'Var' and a 'Type' existentialized over their type index.
  47 data VT src vs = forall t. VT (Var src vs t) (Type src vs t)
  48 deriving instance Source src => Show (VT src vs)
  49
  50 insertSubst :: Var src vs v -> Type src vs v -> Subst src vs -> Subst src vs
  51 insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s
  52
  53 lookupSubst :: Var src vs v -> Subst src vs -> Maybe (Type src vs v)
  54 lookupSubst v (Subst s)
  55  | Just (VT v' t) <- Map.lookup (indexVar v) s
  56  , Just HRefl <- v `eqVarKi` v'
  57  = Just t
  58 lookupSubst _v _m = Nothing
  59
  60 -- * Class 'Substable'
  61 class Substable a where
  62         -- | Like 'substVar', but without the /occurence check/.
  63         substVarUnsafe ::
  64          src ~ SourceOf a =>
  65          vs ~ VarsOf a =>
  66          Var src vs v -> Type src vs v -> a -> a
  67         -- | Substitute all the 'Var's which have a match in given 'Subst'.
  68         subst ::
  69          src ~ SourceOf a =>
  70          vs ~ VarsOf a =>
  71          Subst src vs -> a -> a
  72 instance Substable (Type src vs t) where
  73         substVarUnsafe _v _r t@TyConst{} = t
  74         substVarUnsafe v r (TyApp src f a) =
  75                 TyApp src
  76                  (substVarUnsafe v r f)
  77                  (substVarUnsafe v r a)
  78         substVarUnsafe v r t@(TyVar _src _n vt) =
  79                 case v `eqVarKi` vt of
  80                  Just HRefl -> r
  81                  Nothing -> t
  82         substVarUnsafe v r (TyFam src len fam as) =
  83                 TyFam src len fam $ substVarUnsafe v r as
  84
  85         subst _s t@TyConst{} = t
  86         subst s (TyApp src f a) = TyApp src (subst s f) (subst s a)
  87         subst (Subst s) t@(TyVar _src _n v) =
  88                 case indexVar v `Map.lookup` s of
  89                  Nothing -> t
  90                  Just (VT vr r) ->
  91                         case v `eqVarKi` vr of
  92                          Nothing -> error "[BUG] subst: kind mismatch"
  93                          Just HRefl -> r
  94         subst s (TyFam src len fam as) = TyFam src len fam $ subst s as
  95 instance Substable (Types src vs ts) where
  96         substVarUnsafe _v _r TypesZ = TypesZ
  97         substVarUnsafe v r (TypesS t ts) =
  98                 substVarUnsafe v r t `TypesS`
  99                 substVarUnsafe v r ts
 100         subst _s TypesZ = TypesZ
 101         subst s (TypesS t ts) = subst s t `TypesS` subst s ts
 102
 103 -- | Substitute the given 'Var' by the given 'Type',
 104 -- returning 'Nothing' if this 'Type' contains
 105 -- the 'Var' (occurence check).
 106 substVar ::
 107  src ~ SourceOf a =>
 108  vs ~ VarsOf a =>
 109  Source src => VarOccursIn a => Substable a =>
 110  Var src vs v -> Type src vs v -> a -> Maybe a
 111 substVar v r t =
 112         if v `varOccursIn` r
 113         then Nothing -- NOTE: occurence check
 114         else Just $ substVarUnsafe v r t
 115
 116 -- ** Type 'Error_Unify'
 117 -- | Reasons why two 'Type's cannot be unified.
 118 data Error_Unify src
 119  =   Error_Unify_Var_loop IndexVar (TypeVT src)
 120      -- ^ /occurence check/: a 'Var' is unified with a 'Type'
 121      --   which contains this same 'Var'.
 122  |   Error_Unify_Const_mismatch (TypeVT src) (TypeVT src)
 123      -- ^ Two 'TyConst's should be the same, but are different.
 124  |   Error_Unify_Kind_mismatch (KindK src) (KindK src)
 125      -- ^ Two 'Kind's should be the same, but are different.
 126  |   Error_Unify_Kind (Con_Kind src)
 127      -- ^ Two 'Kind's mismatch.
 128  |   Error_Unify_mismatch (TypeVT src) (TypeVT src)
 129      -- ^ Cannot unify those two 'Type's.
 130
 131 deriving instance Source src => Eq   (Error_Unify src)
 132 deriving instance Source src => Show (Error_Unify src)
 133
 134 instance Inj_Error (Error_Unify src) (Error_Unify src) where
 135         inj_Error = id
 136 instance Inj_Error (Con_Kind src) (Error_Unify src) where
 137         inj_Error = Error_Unify_Kind
 138
 139 -- | Return the left spine of a 'Type':
 140 -- the root 'Type' and its 'Type' parameters,
 141 -- from the left to the right.
 142 spineTy ::
 143  forall src vs t.
 144  Source src =>
 145  Inj_Source (TypeVT src) src =>
 146  Type src vs t ->
 147  (TypeT src vs, [TypeT src vs])
 148 spineTy typ = go [] typ
 149         where
 150         go :: forall x. [TypeT src vs] -> Type src vs x -> (TypeT src vs, [TypeT src vs])
 151         go ctx (TyApp _ (TyApp _ (TyConst _ _ c) _q) t)
 152          | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c
 153          = go ctx t -- NOTE: skip the constraint @q@.
 154         go ctx (TyApp  _src f a) = go (TypeT (a `source` TypeVT typ) : ctx) f
 155         go ctx t = (TypeT (t `source` TypeVT typ), ctx)
 156
 157 {-
 158 spineTy
 159  :: Type src ctx ss cs (t::k)
 160  -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)
 161  -> ret
 162 spineTy = go TypesZ
 163         where
 164         go :: Types src ctx ss cs hs
 165            -> Type src ctx ss cs (t::k)
 166            -> (forall kx (x::kx) xs. Type src ctx ss cs x -> Types src ctx ss cs xs -> ret)
 167            -> ret
 168         go ctx (TyApp  _src f a) k = go (a `TypesS` ctx) f k
 169         go ctx (Term x _te)    k = go ctx x k
 170         go ctx (TyAny x)       k = go ctx x k
 171         go ctx t k = k t ctx
 172 -}
 173
 174 -- | Return the /most general unification/ of two 'Type's, when it exists.
 175 unifyType ::
 176  forall ki (x::ki) (y::ki) vs src.
 177  Inj_Source (TypeVT src) src =>
 178  Inj_Error (Con_Kind src) (Error_Unify src) =>
 179  Subst src vs ->
 180  Type src vs (x::ki) ->
 181  Type src vs (y::ki) ->
 182  Either (Error_Unify src) (Subst src vs)
 183 unifyType vs x y =
 184         let k = kindOfType x in
 185         case (spineTy x, spineTy y) of
 186          ((TypeT hx, px), (TypeT hy, py)) ->
 187                 case (hx, hy) of
 188                  (TyVar _ _n vx, _) | Just Refl <- k `eqKi` kindOfVar vx -> goVar vs vx y
 189                  (_, TyVar _ _n vy) | Just Refl <- k `eqKi` kindOfVar vy -> goVar vs vy x
 190                  (TyConst _sx _lx cx, TyConst _sy _ly cy)
 191                         | Just HRefl <- cx `eqConstKi` cy -> goList vs px py
 192                         | otherwise -> Left $ Error_Unify_Const_mismatch (TypeVT hx) (TypeVT hy)
 193                  _ ->
 194                         case (x, y) of
 195                          (TyApp _ fx ax, TyApp _ fy ay) ->
 196                                 goList vs
 197                                  [TypeT fx, TypeT ax]
 198                                  [TypeT fy, TypeT ay]
 199                          _ -> Left $ Error_Unify_mismatch (TypeVT x) (TypeVT y)
 200         where
 201         goVar ::
 202          forall k (a::k) (b::k) vs'.
 203          Subst src vs' -> Var src vs' a -> Type src vs' b ->
 204          Either (Error_Unify src) (Subst src vs')
 205         goVar vs' va b =
 206                 case va `lookupSubst` vs' of
 207                  Just a -> unifyType vs' b a
 208                  Nothing ->
 209                         case vs' `subst` b of
 210                          TyVar _src _kb vb | Just HRefl <- va `eqVarKi` vb -> Right vs'
 211                          b' | va `varOccursIn` b' -> Left $ Error_Unify_Var_loop (indexVar va) (TypeVT b')
 212                             | Refl :: a :~: b <- unsafeCoerce Refl ->
 213                                 Right $ insertSubst va b' mempty <> vs'
 214         goList ::
 215          forall vs'.
 216          Subst src vs' -> [TypeT src vs'] -> [TypeT src vs'] ->
 217          Either (Error_Unify src) (Subst src vs')
 218         goList vs' [] [] = Right vs'
 219         goList vs' (TypeT a:as) (TypeT b:bs) =
 220                 when_EqKind (kindOfType a) (kindOfType b) $ \Refl ->
 221                 unifyType vs' a b >>= \vs'' -> goList vs'' as bs
 222         goList _vs _a _b = error "[BUG] unifyType: kinds mismatch"