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   Show meta =>
 213   MC.MonadExcept (ErrorUnify meta) m =>
 214   Subst meta vs ->
 215   Ty meta vs (x :: xyK) ->
 216   Ty meta vs (y :: xyK) ->
 217   m (Subst meta vs)
 218 unifyType vs x y =
 219   case (spineTy x, spineTy y) of
 220     ((TyT xRootTy, px), (TyT yRootTy, py)) ->
 221       case (xRootTy, yRootTy) of
 222         (TyVar{tyVar = xV}, _) | Just HRefl <- xK `eqTy` kindOf xV -> goVar vs xV y
 223         (_, TyVar{tyVar = yV}) | Just HRefl <- xK `eqTy` kindOf yV -> goVar vs yV x
 224         (TyConst{tyConst = cx}, TyConst{tyConst = cy})
 225           | Just HRefl <- cx `eqTy` cy -> goZip vs px py
 226           | otherwise -> MC.throw $ ErrorUnifyConst (TyVT xRootTy) (TyVT yRootTy)
 227         _ ->
 228           case (x, y) of
 229             (TyApp fx ax, TyApp fy ay) -> goZip vs [TyT fx, TyT ax] [TyT fy, TyT ay]
 230             _ -> MC.throw $ ErrorUnifyType (TyVT x) (TyVT y)
 231   where
 232     xK = kindOf x
 233     goVar ::
 234       forall k (a :: k) (b :: k) ws.
 235       Subst meta ws ->
 236       Var meta ws a ->
 237       Ty meta ws b ->
 238       m (Subst meta ws)
 239     goVar ws va b =
 240       case va `lookupSubst` ws of
 241         Just a -> unifyType ws b a
 242         Nothing ->
 243           case ws `subst` b of
 244             TyVar{tyVar = vb} | Just HRefl <- va `eqTy` vb -> return ws
 245             b'
 246               | va `varOccursIn` b' -> MC.throw $ ErrorUnifyVarLoop (indexVar va) (TyVT b')
 247               | HRefl :: a :~~: b <- unsafeCoerce HRefl ->
 248                   return $ insertSubst va b' mempty <> ws
 249     goZip ::
 250       forall ws.
 251       Subst meta ws ->
 252       [TyT meta ws] ->
 253       [TyT meta ws] ->
 254       m (Subst meta ws)
 255     goZip ws [] [] = return ws
 256     goZip ws (TyT a : as) (TyT b : bs) =
 257       case aK `eqTy` bK of
 258         Nothing -> MC.throw $ ErrorUnifyKind (TyT aK) (TyT bK)
 259         Just HRefl -> unifyType ws a b >>= \ws' -> goZip ws' as bs
 260       where
 261         aK = kindOf a
 262         bK = kindOf b
 263     goZip _vs _a _b = Prelude.error "[BUG] unifyType: kinds mismatch"