symantic/Language/Symantic/Typing/Unify.hs

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