-- | 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           SrcLoc
import           Text.PrettyPrint.HughesPJ (Doc)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.RefType ()
-- import           Language.Haskell.Liquid.UX.Tidy
import           TyCon                                  hiding (tyConName)

meetVarTypes :: F.TCEmb TyCon -> Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
meetVarTypes :: TCEmb TyCon
-> Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
meetVarTypes TCEmb TyCon
_emb Doc
_v (SrcSpan, SpecType)
hs (SrcSpan, SpecType)
lq = {- meetError emb err -} SpecType -> SpecType -> SpecType
forall r. Reftable r => r -> r -> r
F.meet SpecType
hsT SpecType
lqT
  where
    (SrcSpan
_hsSp, SpecType
hsT)      = (SrcSpan, SpecType)
hs
    (SrcSpan
_lqSp, SpecType
lqT)      = (SrcSpan, SpecType)
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 `F.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

-}