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