content: ------------------------------------------------------------------------------
  -- Copyright 2012-2021, Microsoft Research, Daan Leijen.
  --
  -- This is free software; you can redistribute it and/or modify it under the
  -- terms of the Apache License, Version 2.0. A copy of the License can be
  -- found in the LICENSE file at the root of this distribution.
  -----------------------------------------------------------------------------
  {--}
  -----------------------------------------------------------------------------
  
  module Kind.Unify( Context(..), unify, mgu, match ) where
  
  import Lib.PPrint
  import Common.Range
  import Common.Message( docFromRange, table)
  
  import Kind.Kind
  import Kind.InferKind
  import Kind.InferMonad
  
  
  {---------------------------------------------------------------
    Unify
  ---------------------------------------------------------------}
  data Context = Check String Range
               | Infer Range
  
  unify :: Context -> Range -> InfKind -> InfKind -> KInfer ()
  unify context range kind1 kind2
    = do skind1 <- subst kind1
         skind2 <- subst kind2
         -- trace ("unify: " ++ show skind1 ++ " and " ++ show skind2) $
         case mgu skind1 skind2 of
           Ok sub' -> extendKSub sub'
           err     -> do cscheme <- getColorScheme
                         kindError cscheme context range err skind1 skind2
  
  kindError colors context range err kind1 kind2
    = addError range $
      text message <->
      table ([(text "type context", docFromRange colors rangeContext)
             ,(text "type", docFromRange colors range)
             ,(text "inferred kind", niceKind2)
             ,(text expected, niceKind1)
             ]
             ++ extra)
    where
      (rangeContext,expected,extra)
        = case context of
            Check msg range -> (range,"expected kind",[(text "because", text msg)])
            Infer range     -> (range,"expected kind",inferExtra)
  
      inferExtra
        = if (isInfKindScope kind1 || isInfKindScope kind2)
           then [(text "hint", text "scoped effects need a first type parameter annotated with kind \"::S\"")]
           else []
  
      [niceKind1,niceKind2]
        = niceInfKinds colors [kind1,kind2]
  
      message
        = case err of
            InfiniteKind -> "Invalid type (due to an infinite kind)"
            _            -> "Invalid type"
  
  
  
  
  {---------------------------------------------------------------
    MGU
  ---------------------------------------------------------------}
  data Unify = Ok KSub
             | InfiniteKind
             | NoMatch
  
  mgu :: InfKind -> InfKind -> Unify
  -- constants
  mgu (KIVar id1) (KIVar id2)  | id1 == id2
    = Ok ksubEmpty
  mgu (KICon kind1) (KICon kind2)
    = if (match kind1 kind2)
       then Ok ksubEmpty
       else NoMatch
  mgu (KIApp k1 k2) (KIApp l1 l2)
    = case mgu k1 l1 of
        Ok sub1 -> case mgu (sub1 |=> k2) (sub1 |=> l2) of
                       Ok sub2 -> Ok (sub2 @@ sub1)
                       err -> err
        err -> err
  
  -- pull up KApp's
  mgu (KICon (KApp k1 k2)) (KIApp l1 l2)
    = mgu (KIApp (KICon k1) (KICon k2)) (KIApp l1 l2)
  
  mgu (KIApp k1 k2) (KICon (KApp l1 l2))
    = mgu (KIApp k1 k2) (KIApp (KICon l1) (KICon l2))
  
  -- unify variables
  mgu (KIVar id) kind
    = unifyVar id kind
  mgu kind (KIVar id)
    = unifyVar id kind
  
  -- no match
  mgu _ _
    = NoMatch
  
  unifyVar id kind
    = if kvsMember id (fkv kind)
       then InfiniteKind
       else Ok (ksubSingle id kind)
  
  match :: Kind -> Kind -> Bool
  match (KCon c1) (KCon c2)         = (c1 == c2)
  match (KApp k1 k2) (KApp l1 l2)   = (match k1 l1) && (match k2 l2)
  match _ _ = False
  