-- | This code has various wrappers around `meet` and `strengthen`
--   that are here so that we can throw decent error messages if
--   they fail. The module depends on `RefType` and `UX.Tidy`.

module Language.Haskell.Liquid.Types.Meet ( meetVarTypes ) where

import           Text.PrettyPrint.HughesPJ (Doc)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RefType ()
import           Liquid.GHC.API as Ghc

meetVarTypes :: F.TCEmb TyCon -> Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
meetVarTypes :: TCEmb TyCon
-> Doc
-> (SrcSpan, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (SrcSpan, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
meetVarTypes TCEmb TyCon
_emb Doc
_v (SrcSpan, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
hs (SrcSpan, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lq = {- meetError emb err -} RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. Meet r => r -> r -> r
meet RTypeBV Symbol Symbol RTyCon RTyVar RReft
hsT RTypeBV Symbol Symbol RTyCon RTyVar RReft
lqT
  where
    (SrcSpan
_hsSp, RTypeBV Symbol Symbol RTyCon RTyVar RReft
hsT)      = (SrcSpan, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
hs
    (SrcSpan
_lqSp, RTypeBV Symbol Symbol RTyCon RTyVar RReft
lqT)      = (SrcSpan, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lq
    -- _err              = ErrMismatch lqSp v (text "meetVarTypes") hsD lqD hsSp
    -- _hsD              = F.pprint hsT
    -- _lqD              = F.pprint lqT
{-

_meetError :: F.TCEmb TyCon -> Error -> SpecType -> SpecType -> SpecType
_meetError _emb _e t t'
  -- // | meetable emb t t'
  | True              = t `meet` t'
  -- // | otherwise         = panicError e

_meetable :: F.TCEmb TyCon -> SpecType -> SpecType -> Bool
_meetable _emb t1 t2 = F.notracepp ("meetable: " ++  showpp (s1, t1, s2, t2)) (s1 == s2)
  where
    s1              = tx t1
    s2              = tx t2
    tx              = rTypeSort _emb . toRSort

-}