src/Symantic/Typer/Unify.hs

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