src/Symantic/Typer/Unify.hs

   1 {-# LANGUAGE ExistentialQuantification #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE StandaloneDeriving #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# OPTIONS_GHC -fno-warn-orphans #-}
   6
   7 module Symantic.Typer.Unify where
   8
   9 import Control.Monad (Monad (..))
  10 import Control.Monad.Classes as MC (MonadExcept, throw)
  11 import Control.Monad.Classes.Run as MC ()
  12 import Data.Bool (otherwise)
  13 import Data.Eq (Eq (..))
  14 import Data.Function (id, ($))
  15 import Data.Functor ((<$>))
  16 import Data.Map.Strict (Map)
  17 import Data.Map.Strict qualified as Map
  18 import Data.Maybe (Maybe (..))
  19 import Data.Monoid (Monoid (..))
  20 import Data.Semigroup (Semigroup (..))
  21 import Text.Show (Show)
  22 import Type.Reflection ((:~~:) (HRefl))
  23 import Unsafe.Coerce (unsafeCoerce)
  24 import Prelude qualified
  25
  26 import Symantic.Parser.Error (ErrorInj (..))
  27 import Symantic.Typer.Eq (EqTy (eqTy))
  28 import Symantic.Typer.Type (
  29   IndexVar,
  30   KindK,
  31   KindOf (kindOf),
  32   Ty (TyApp, TyConst, TyVar, tyConst, tyVar),
  33   TyT (..),
  34   TyVT (..),
  35   Tys (..),
  36   Var,
  37   VarOccursIn (..),
  38   indexVar,
  39   proj_ConstKi,
  40   type (#>),
  41  )
  42
  43 -- import Symantic.Typer.Show ()
  44
  45 -- * Type 'Subst'
  46
  47 -- | /Type variable substitution/.
  48 --
  49 -- WARNING: a 'Subst' MUST be without loops, and fully expanded.
  50 newtype Subst meta vs
  51   = Subst (Map IndexVar (VT meta vs))
  52
  53 deriving instance (Show meta, Monoid meta) => Show (Subst meta vs)
  54 instance Monoid meta => Semigroup (Subst meta vs) where
  55   (<>) = unionSubst
  56 instance Monoid meta => Monoid (Subst meta vs) where
  57   mempty = Subst Map.empty
  58   mappend = (<>)
  59
  60 -- | Unify two 'Subst's.
  61 --
  62 -- NOTE: the union is left-biased: in case of duplicate 'Var's,
  63 -- it keeps the one from the first 'Subst' given.
  64 --
  65 -- NOTE: the first 'Subst' given is applied to the second (with 'subst'),
  66 -- this way each 'Var' directly maps to an expanded 'Type',
  67 -- so that, when using the resulting 'Subst',
  68 -- there is no need to apply it multiple times
  69 -- until there is no more substitution to be done.
  70 unionSubst :: Subst meta vs -> Subst meta vs -> Subst meta vs
  71 unionSubst sx@(Subst x) (Subst y) = Subst $ x `Map.union` ((\(VT v r) -> VT v $ subst sx r) Data.Functor.<$> y)
  72
  73 -- * Type 'VT'
  74
  75 -- | A 'Var' and a 'Type' existentialized over their type index.
  76 data VT meta vs = forall t. VT (Var meta vs t) (Ty meta vs t)
  77
  78 deriving instance (Show meta, Monoid meta) => Show (VT meta vs)
  79
  80 insertSubst :: Monoid meta => Var meta vs v -> Ty meta vs v -> Subst meta vs -> Subst meta vs
  81 insertSubst v t (Subst s) = Subst $ Map.insert (indexVar v) (VT v t) s
  82
  83 lookupSubst :: Monoid meta => Var meta vs v -> Subst meta vs -> Maybe (Ty meta vs v)
  84 lookupSubst v (Subst s)
  85   | Just (VT v' t) <- Map.lookup (indexVar v) s
  86   , Just HRefl <- v `eqTy` v' =
  87       Just t
  88 lookupSubst _v _m = Nothing
  89
  90 -- * Class 'Substable'
  91 class Substable t where
  92   -- | Like 'substVar', but without the /occurence check/.
  93   substVarUnsafe ::
  94     Var meta vs v -> Ty meta vs v -> t meta vs a -> t meta vs a
  95
  96   -- | Substitute all the 'Var's which have a match in given 'Subst'.
  97   subst ::
  98     Subst meta vs -> t meta vs a -> t meta vs a
  99 instance Substable Ty where
 100   substVarUnsafe _v _r t@TyConst{} = t
 101   substVarUnsafe v r (TyApp f a) =
 102     TyApp
 103       (substVarUnsafe v r f)
 104       (substVarUnsafe v r a)
 105   substVarUnsafe v r t@TyVar{tyVar = tv} =
 106     case v `eqTy` tv of
 107       Just HRefl -> r
 108       Nothing -> t
 109
 110   -- substVarUnsafe v r (TyFam meta len fam as) =
 111   --  TyFam meta len fam $ substVarUnsafe v r as
 112
 113   subst _s t@TyConst{} = t
 114   subst s (TyApp f a) = TyApp (subst s f) (subst s a)
 115   subst (Subst s) t@TyVar{tyVar = tv} =
 116     case Map.lookup (indexVar tv) s of
 117       Nothing -> t
 118       Just (VT vr r) ->
 119         case tv `eqTy` vr of
 120           Nothing -> Prelude.error "[BUG] subst: kind mismatch"
 121           Just HRefl -> r
 122
 123 -- subst s (TyFam meta len fam as) = TyFam meta len fam $ subst s as
 124 instance Substable (Tys as) where
 125   substVarUnsafe _v _r TysZ = TysZ
 126   substVarUnsafe v r (TysS t ts) =
 127     substVarUnsafe v r t
 128       `TysS` substVarUnsafe v r ts
 129   subst _s TysZ = TysZ
 130   subst s (TysS t ts) = subst s t `TysS` subst s ts
 131
 132 -- | Substitute the given 'Var' by the given 'Type',
 133 -- returning 'Nothing' if this 'Type' contains
 134 -- the 'Var' (occurence check).
 135 substVar ::
 136   VarOccursIn t =>
 137   Substable t =>
 138   Var meta vs v ->
 139   Ty meta vs v ->
 140   t meta vs a ->
 141   Maybe (t meta vs a)
 142 substVar v r t =
 143   if v `varOccursIn` r
 144     then Nothing -- NOTE: occurence check
 145     else Just $ substVarUnsafe v r t
 146
 147 -- ** Type 'ErrorUnify'
 148
 149 -- | Reasons why two 'Type's cannot be unified.
 150 data ErrorUnify meta
 151   = -- | /occurence check/: a 'Var' is unified with a 'Type'
 152     --   which contains this same 'Var'.
 153     ErrorUnifyVarLoop IndexVar (TyVT meta)
 154   | -- | Two 'TyConst's should be the same, but are different.
 155     ErrorUnifyConst (TyVT meta) (TyVT meta)
 156   | -- | Two 'Kind's should be the same, but are different.
 157     ErrorUnifyKind (KindK meta) (KindK meta)
 158   | -- | Cannot unify those two 'Type's.
 159     ErrorUnifyType (TyVT meta) (TyVT meta)
 160
 161 deriving instance Monoid meta => Eq (ErrorUnify meta)
 162 deriving instance (Show meta, Monoid meta) => Show (ErrorUnify meta)
 163
 164 instance ErrorInj (ErrorUnify meta) (ErrorUnify meta) where
 165   errorInj = id
 166
 167 data SourceTypeArg meta
 168   = SourceTypeArg (TyVT meta)
 169
 170 -- | Return the left spine of a 'Ty':
 171 -- the root 'Ty' and its 'Ty' parameters,
 172 -- from the left to the right.
 173 spineTy ::
 174   forall meta vs t.
 175   -- MC.MonadWriter (SourceTypeArg meta) (Sourced meta) =>
 176   Ty meta vs t ->
 177   (TyT meta vs, [TyT meta vs])
 178 spineTy = go []
 179   where
 180     go :: forall kx (x :: kx). [TyT meta vs] -> Ty meta vs x -> (TyT meta vs, [TyT meta vs])
 181     -- Skip the constraint @q@.
 182     go ctx (TyApp (TyApp (TyConst{tyConst = c}) _q) t)
 183       | Just HRefl <- proj_ConstKi @_ @(#>) c =
 184           go ctx t
 185     -- Add a type to the spine.
 186     go ctx (TyApp f a) = go (TyT a {-(SourceTypeArg (TyVT ty)-} : ctx) f
 187     -- Add the root.
 188     go ctx t = (TyT t {-SourceTypeArg (TyVT ty)-}, ctx)
 189
 190 {-
 191 spineTy
 192  :: Ty meta ctx ss cs (t::k)
 193  -> (forall kx (x::kx) xs. Ty meta ctx ss cs x -> Tys meta ctx ss cs xs -> ret)
 194  -> ret
 195 spineTy = go TysZ
 196   where
 197   go :: Tys meta ctx ss cs hs
 198      -> Ty meta ctx ss cs (t::k)
 199      -> (forall kx (x::kx) xs. Ty meta ctx ss cs x -> Tys meta ctx ss cs xs -> ret)
 200      -> ret
 201   go ctx (TyApp  _src f a) k = go (a `TysS` ctx) f k
 202   go ctx (Term x _te)    k = go ctx x k
 203   go ctx (TyAny x)       k = go ctx x k
 204   go ctx t k = k t ctx
 205 -}
 206
 207 -- | Return the /most general unification/ of two 'Type's, when it exists.
 208 unifyType ::
 209   forall xyK (x :: xyK) (y :: xyK) vs meta m.
 210   -- ErrorInj (Con_Kind meta) (ErrorUnify meta) =>
 211   Monoid meta =>
 212   MC.MonadExcept (ErrorUnify meta) m =>
 213   Subst meta vs ->
 214   Ty meta vs (x :: xyK) ->
 215   Ty meta vs (y :: xyK) ->
 216   m (Subst meta vs)
 217 unifyType vs x y =
 218   case (spineTy x, spineTy y) of
 219     ((TyT xRootTy, px), (TyT yRootTy, py)) ->
 220       case (xRootTy, yRootTy) of
 221         (TyVar{tyVar = xV}, _) | Just HRefl <- xK `eqTy` kindOf xV -> goVar vs xV y
 222         (_, TyVar{tyVar = yV}) | Just HRefl <- xK `eqTy` kindOf yV -> goVar vs yV x
 223         (TyConst{tyConst = cx}, TyConst{tyConst = cy})
 224           | Just HRefl <- cx `eqTy` cy -> goZip vs px py
 225           | otherwise -> MC.throw $ ErrorUnifyConst (TyVT xRootTy) (TyVT yRootTy)
 226         _ ->
 227           case (x, y) of
 228             (TyApp fx ax, TyApp fy ay) -> goZip vs [TyT fx, TyT ax] [TyT fy, TyT ay]
 229             _ -> MC.throw $ ErrorUnifyType (TyVT x) (TyVT y)
 230   where
 231     xK = kindOf x
 232     goVar ::
 233       forall k (a :: k) (b :: k) ws.
 234       Subst meta ws ->
 235       Var meta ws a ->
 236       Ty meta ws b ->
 237       m (Subst meta ws)
 238     goVar ws va b =
 239       case va `lookupSubst` ws of
 240         Just a -> unifyType ws b a
 241         Nothing ->
 242           case ws `subst` b of
 243             TyVar{tyVar = vb} | Just HRefl <- va `eqTy` vb -> return ws
 244             b'
 245               | va `varOccursIn` b' -> MC.throw $ ErrorUnifyVarLoop (indexVar va) (TyVT b')
 246               | HRefl :: a :~~: b <- unsafeCoerce HRefl ->
 247                   return $ insertSubst va b' mempty <> ws
 248     goZip ::
 249       forall ws.
 250       Subst meta ws ->
 251       [TyT meta ws] ->
 252       [TyT meta ws] ->
 253       m (Subst meta ws)
 254     goZip ws [] [] = return ws
 255     goZip ws (TyT a : as) (TyT b : bs) =
 256       case aK `eqTy` bK of
 257         Nothing -> MC.throw $ ErrorUnifyKind (TyT aK) (TyT bK)
 258         Just HRefl -> unifyType ws a b >>= \ws' -> goZip ws' as bs
 259       where
 260         aK = kindOf a
 261         bK = kindOf b
 262     goZip _vs _a _b = Prelude.error "[BUG] unifyType: kinds mismatch"