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