Drop only dictionaries of type Eq, Ord, Numerical, and ~

src/Language/Haskell/Liquid/Bare/Axiom.hs

@@ -178,7 +178,7 @@ axiomType s t = AT to (reverse xts) res
     (to, (_,xts, Just res)) = runState (go t) (1,[], Nothing)
     go (RAllT a t r) = RAllT a <$> go t <*> return r 
     go (RAllP p t) = RAllP p <$> go t 
-    go (RFun x tx t r) | isClassType tx = (\t' -> RFun x tx t' r) <$> go t
+    go (RFun x tx t r) | isEmbeddedClass tx = (\t' -> RFun x tx t' r) <$> go t
     go (RFun x tx t r) = do 
       (i,bs,res) <- get 
       let x' = unDummy x i 

src/Language/Haskell/Liquid/Constraint/Generate.hs

@@ -318,7 +318,7 @@ consCBSizedTys γ xes
        let rts   = (recType autoenv <$>) <$> xeets
        let xts   = zip xs ts
        γ'       <- foldM extender γ xts
-       let γs    = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isPredVar) <$> vs)
+       let γs    = zipWith makeRecInvariants [γ' `setTRec` zip xs rts' | rts' <- rts] (filter (not . GM.isEmbeddedDictVar) <$> vs)
        let xets' = zip3 xs es ts
        mapM_ (uncurry $ consBind True) (zip γs xets')
        return γ'
@@ -724,7 +724,7 @@ splitConstraints :: TyConable c
                  => RType c tv r -> ([[(F.Symbol, RType c tv r)]], RType c tv r)
 splitConstraints (RRTy cs _ OCons t)
   = let (css, t') = splitConstraints t in (cs:css, t')
-splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isClass c
+splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isEmbeddedDict c
   = let (css, t') = splitConstraints t in (css, RFun x tx t' r)
 splitConstraints t
   = ([], t)
@@ -1122,7 +1122,7 @@ dropExists γ (REx x tx t) =         (, t) <$> γ += ("dropExists", x, tx)
 dropExists γ t            = return (γ, t)
 
 dropConstraints :: CGEnv -> SpecType -> CG SpecType
-dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isClass c
+dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isEmbeddedDict c
   = (flip (RFun x tx)) r <$> dropConstraints γ t
 dropConstraints γ (RRTy cts _ OCons t)
   = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ xts
@@ -1161,7 +1161,7 @@ caseEnv γ x _   (DataAlt c) ys pIs = do
   tdc             <- (γ ??= (dataConWorkId c) >>= refreshVV)
   let (rtd,yts',_) = unfoldR tdc xt ys
   yts             <- projectTypes pIs yts'
-  let ys''         = F.symbol <$> filter (not . GM.isPredVar) ys
+  let ys''         = F.symbol <$> filter (not . GM.isEmbeddedDictVar) ys
   let r1           = dataConReft   c   ys''
   let r2           = dataConMsReft rtd ys''
   let xt           = (xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2))
@@ -1305,7 +1305,7 @@ lamExpr γ (Lit c)     = snd  $ literalConst (emb γ) c
 lamExpr γ (Tick _ e)  = lamExpr γ e
 lamExpr γ (App e (Type _)) = lamExpr γ e
 lamExpr γ (App e1 e2) = case (lamExpr γ e1, lamExpr γ e2) of
-                              (Just p1, Just p2) | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2)
+                              (Just p1, Just p2) | not (GM.isEmbeddedDictExpr e2) -- (isClassPred $ exprType e2)
                                                  -> Just $ F.EApp p1 p2
                               (Just p1, Just _ ) -> Just p1
                               _  -> Nothing
@@ -1357,7 +1357,7 @@ makeSingleton γ e t
   | higherOrderFlag γ, App f x <- simplify e
   = case (funExpr γ f, argForAllExpr x) of
       (Just f', Just x')
-                 | not (GM.isPredExpr x) -- (isClassPred $ exprType x)
+                 | not (GM.isEmbeddedDictExpr x) -- (isClassPred $ exprType x)
                  -> strengthenMeet t (uTop $ F.exprReft (F.EApp f' x'))
       (Just f', Just _)
                  -> strengthenMeet t (uTop $ F.exprReft f')
@@ -1390,7 +1390,7 @@ funExpr γ (Var v) | S.member v (fargs γ) || GM.isDataConId v
 
 funExpr γ (App e1 e2)
   = case (funExpr γ e1, argExpr γ e2) of
-      (Just e1', Just e2') | not (GM.isPredExpr e2) -- (isClassPred $ exprType e2)
+      (Just e1', Just e2') | not (GM.isEmbeddedDictExpr e2) -- (isClassPred $ exprType e2)
                            -> Just (F.EApp e1' e2')
       (Just e1', Just _)
                            -> Just e1'

src/Language/Haskell/Liquid/Constraint/Split.hs

@@ -249,7 +249,7 @@ splitC (SubC γ t1'@(RAllT α1 t1 _) t2'@(RAllT α2 t2 _))
           (Just (x1, _), Just (x2, _)) -> F.mkSubst [(x1, F.EVar x2)]
           _                            -> F.mkSubst []
 
-splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isClass c1 && c1 == c2
+splitC (SubC _ (RApp c1 _ _ _) (RApp c2 _ _ _)) | isEmbeddedDict c1 && c1 == c2
   = return []
 
 splitC (SubC γ t1@(RApp _ _ _ _) t2@(RApp _ _ _ _))

src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs

@@ -184,7 +184,7 @@ specTypeToLogic es e t
 
 
     su           = F.mkSubst $ zip xs es
-    (cls, nocls) = L.partition (isClassType.snd) $ zip (ty_binds trep) (ty_args trep)
+    (cls, nocls) = L.partition (isEmbeddedClass.snd) $ zip (ty_binds trep) (ty_args trep)
                  :: ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)])
     (xs, ts)     = unzip nocls :: ([F.Symbol], [SpecType])
 

src/Language/Haskell/Liquid/GHC/Misc.hs

@@ -19,7 +19,7 @@ module Language.Haskell.Liquid.GHC.Misc where
 import           Class                                      (classKey)
 import           Data.String
 import qualified Data.List as L
-import           PrelNames                                  (fractionalClassKeys)
+import           PrelNames                                  (fractionalClassKeys, itName, ordClassKey, numericClassKeys, eqClassKey)
 import           FamInstEnv
 import           Debug.Trace
 -- import qualified ConLike                                    as Ghc
@@ -56,7 +56,7 @@ import           TcRnDriver
 
 
 import           RdrName
-import           Type                                       (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind)
+import           Type                                       (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind, tyConAppTyCon_maybe)
 import           TyCoRep
 import           Var
 import           IdInfo
@@ -219,6 +219,9 @@ unTickExpr x                  = x
 isFractionalClass :: Class -> Bool
 isFractionalClass clas = classKey clas `elem` fractionalClassKeys
 
+isOrdClass :: Class -> Bool
+isOrdClass clas = classKey clas == ordClassKey
+
 --------------------------------------------------------------------------------
 -- | Pretty Printers -----------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -802,6 +805,47 @@ binders (Rec xes)    = fst <$> xes
 
 expandVarType :: Var -> Type
 expandVarType = expandTypeSynonyms . varType
+
+--------------------------------------------------------------------------------
+-- | The following functions test if a `CoreExpr` or `CoreVar` can be
+--   embedded in logic. With type-class support, we can no longer erase
+--   such expressions arbitrarily.
+--------------------------------------------------------------------------------
+isEmbeddedDictExpr :: CoreExpr -> Bool
+isEmbeddedDictExpr = isEmbeddedDictType . CoreUtils.exprType
+
+isEmbeddedDictVar :: Var -> Bool
+isEmbeddedDictVar v = F.notracepp msg . isEmbeddedDictType . varType $ v
+  where
+    msg     =  "isGoodCaseBind v = " ++ show v
+
+isEmbeddedDictType :: Type -> Bool
+isEmbeddedDictType = anyF [isOrdPred, isNumericPred, isEqPred, isPrelEqPred]
+
+-- unlike isNumCls, isFracCls, these two don't check if the argument's
+-- superclass is Ord or Num. I believe this is the more predictable behavior
+
+isPrelEqPred :: Type -> Bool
+isPrelEqPred ty = case tyConAppTyCon_maybe ty of
+  Just tyCon -> isPrelEqTyCon tyCon
+  _          -> False
+
+
+isPrelEqTyCon :: TyCon -> Bool
+isPrelEqTyCon tc = tc `hasKey` eqClassKey
+
+isOrdPred :: Type -> Bool
+isOrdPred ty = case tyConAppTyCon_maybe ty of
+  Just tyCon -> tyCon `hasKey` ordClassKey
+  _          -> False
+
+-- Not just Num, but Fractional, Integral as well
+isNumericPred :: Type -> Bool
+isNumericPred ty = case tyConAppTyCon_maybe ty of
+  Just tyCon -> getUnique tyCon `elem` numericClassKeys
+  _          -> False
+
+
 --------------------------------------------------------------------------------
 -- | The following functions test if a `CoreExpr` or `CoreVar` are just types
 --   in disguise, e.g. have `PredType` (in the GHC sense of the word), and so

src/Language/Haskell/Liquid/LawInstances.hs

@@ -90,6 +90,6 @@ splitTypeConstraints :: [(F.Symbol, SpecType)] -> ([(F.Symbol, SpecType)], [(F.S
 splitTypeConstraints = go []  
   where  
     go cs (b@(_x, RApp c _ _ _):ts) 
-      | isClass c
+      | isEmbeddedDict c
       = go (b:cs) ts 
     go cs r = (reverse cs, map (\(x, t) -> (x, shiftVV t x)) r)

src/Language/Haskell/Liquid/Measure.hs

@@ -261,7 +261,7 @@ mapArgumens lc t1 t2 = go xts1' xts2'
     xts1' = dropWhile canDrop xts1
     xts2' = dropWhile canDrop xts2
 
-    canDrop (_, t) = isClassType t || isEqType t
+    canDrop (_, t) = isEmbeddedClass t
 
     go xs ys
       | length xs == length ys && and (zipWith (==) (toRSort . snd <$> xts1') (toRSort . snd <$> xts2'))

src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs

@@ -63,7 +63,7 @@ logicType :: (Reftable r) => Type -> RRType r
 logicType τ      = fromRTypeRep $ t { ty_binds = bs, ty_args = as, ty_refts = rs}
   where
     t            = toRTypeRep $ ofType τ
-    (bs, as, rs) = unzip3 $ dropWhile (isClassType . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t)
+    (bs, as, rs) = unzip3 $ dropWhile (isEmbeddedClass . Misc.snd3) $ zip3 (ty_binds t) (ty_args t) (ty_refts t)
 
 {- | [NOTE:inlineSpecType type]: the refinement depends on whether the result type is a Bool or not:
       CASE1: measure f@logic :: X -> Bool <=> f@haskell :: x:X -> {v:Bool | v <=> (f@logic x)}
@@ -77,7 +77,7 @@ inlineSpecType v = fromRTypeRep $ rep {ty_res = res `strengthen` r , ty_binds =
     rep            = toRTypeRep t
     res            = ty_res rep
     xs             = intSymbol (symbol ("x" :: String)) <$> [1..length $ ty_binds rep]
-    vxs            = dropWhile (isClassType . snd) $ zip xs (ty_args rep)
+    vxs            = dropWhile (isEmbeddedClass . snd) $ zip xs (ty_args rep)
     f              = dummyLoc (symbol v)
     t              = ofType (GM.expandVarType v) :: SpecType
     mkA            = EVar . fst 
@@ -104,7 +104,7 @@ measureSpecType v = go mkT [] [1..] t
     go f args i (RAllT a t r)    = RAllT a (go f args i t) r 
     go f args i (RAllP p t)      = RAllP p $ go f args i t
     go f args i (RFun x t1 t2 r)
-     | isClassType t1           = RFun x t1 (go f args i t2) r
+     | isEmbeddedClass t1           = RFun x t1 (go f args i t2) r
     go f args i t@(RFun _ t1 t2 r)
      | hasRApps t               = RFun x' t1 (go f (x':args) (tail i) t2) r
                                        where x' = intSymbol (symbol ("x" :: String)) (head i)
@@ -127,7 +127,7 @@ weakenResult v t = F.notracepp msg t'
     rep          = toRTypeRep t
     weaken x     = pAnd . filter ((Just vE /=) . isSingletonExpr x) . conjuncts 
     vE           = mkEApp vF xs
-    xs           = EVar . fst <$> dropWhile (isClassType . snd) xts 
+    xs           = EVar . fst <$> dropWhile (isEmbeddedClass . snd) xts 
     xts          = zip (ty_binds rep) (ty_args rep)
     vF           = dummyLoc (symbol v)
 

src/Language/Haskell/Liquid/Types/Fresh.hs

@@ -91,7 +91,7 @@ trueRefType (RImpF _ t t' _)
 trueRefType (RFun _ t t' _)
   = rFun <$> fresh <*> true t <*> true t'
 
-trueRefType (RApp c ts _  _) | isClass c
+trueRefType (RApp c ts _  _) | isEmbeddedDict c
   = rRCls c <$> mapM true ts
 
 trueRefType (RApp c ts rs r)
@@ -144,7 +144,7 @@ refreshRefType (RFun b t t' _)
   | b == F.dummySymbol = rFun <$> fresh <*> refresh t <*> refresh t'
   | otherwise          = rFun     b     <$> refresh t <*> refresh t'
 
-refreshRefType (RApp rc ts _ _) | isClass rc
+refreshRefType (RApp rc ts _ _) | isEmbeddedDict rc
   = return $ rRCls rc ts
 
 refreshRefType (RApp rc ts rs r)

src/Language/Haskell/Liquid/Types/RefType.hs

@@ -150,7 +150,7 @@ dataConArgs trep = unzip [ (x, t) | (x, t) <- zip xs ts, isValTy t]
   where
     xs           = ty_binds trep
     ts           = ty_args trep
-    isValTy      = not . GM.isPredType . toType
+    isValTy      = not . GM.isEmbeddedDictType . toType
 
 
 pdVar :: PVar t -> Predicate

src/Language/Haskell/Liquid/Types/Types.hs

@@ -52,7 +52,7 @@ module Language.Haskell.Liquid.Types.Types (
   , rTyConPVs
   , rTyConPropVs
   -- , isClassRTyCon
-  , isClassType, isEqType, isRVar, isBool
+  , isClassType, isEqType, isRVar, isBool, isEmbeddedClass
 
   -- * Refinement Types
   , RType (..), Ref(..), RTProp, rPropP
@@ -616,6 +616,11 @@ isClassType :: TyConable c => RType c t t1 -> Bool
 isClassType (RApp c _ _ _) = isClass c
 isClassType _              = False
 
+isEmbeddedClass :: TyConable c => RType c t t1 -> Bool
+isEmbeddedClass (RApp c _ _ _) = isEmbeddedDict c
+isEmbeddedClass _              = False
+
+
 -- rTyConPVHPs = filter isHPropPV . rtc_pvars
 -- isHPropPV   = not . isPropPV
 
@@ -896,15 +901,20 @@ class (Eq c) => TyConable c where
   isTuple  :: c -> Bool
   ppTycon  :: c -> Doc
   isClass  :: c -> Bool
+  isEmbeddedDict :: c -> Bool
   isEqual  :: c -> Bool
 
   isNumCls  :: c -> Bool
   isFracCls :: c -> Bool
+  isOrdCls  :: c -> Bool
+  isEqCls   :: c -> Bool
 
-  isClass   = const False
-  isEqual   = const False
-  isNumCls  = const False
-  isFracCls = const False
+  isClass          = const False
+  isEmbeddedDict c = isNumCls c || isEqual c || isOrdCls c || isEqCls c
+  isEqual          = const False
+  isNumCls         = const False
+  isFracCls        = const False
+  isOrdCls         = const False
 
 
 -- Should just make this a @Pretty@ instance but its too damn tedious
@@ -929,10 +939,13 @@ instance TyConable RTyCon where
   isEqual    = isEqual . rtc_tc
   ppTycon    = F.toFix
 
-  isNumCls c  = maybe False (isClassOrSubClass isNumericClass)
+  isNumCls c  = maybe False isNumericClass
+                (tyConClass_maybe $ rtc_tc c)
+  isFracCls c = maybe False isFractionalClass
                 (tyConClass_maybe $ rtc_tc c)
-  isFracCls c = maybe False (isClassOrSubClass isFractionalClass)
+  isOrdCls c  = maybe False isOrdClass
                 (tyConClass_maybe $ rtc_tc c)
+  isEqCls  c  = isEqCls (rtc_tc c)
 
 
 instance TyConable TyCon where
@@ -943,10 +956,13 @@ instance TyConable TyCon where
   isEqual c  = c == eqPrimTyCon || c == eqReprPrimTyCon
   ppTycon    = text . showPpr
 
-  isNumCls c  = maybe False (isClassOrSubClass isNumericClass)
-                (tyConClass_maybe $ c)
-  isFracCls c = maybe False (isClassOrSubClass isFractionalClass)
-                (tyConClass_maybe $ c)
+  isNumCls c  = maybe False isNumericClass
+                (tyConClass_maybe c)
+  isFracCls c = maybe False isFractionalClass
+                (tyConClass_maybe c)
+  isOrdCls c  = maybe False isOrdClass
+                (tyConClass_maybe c)
+  isEqCls  c  = isPrelEqTyCon c
 
 
 isClassOrSubClass :: (Class -> Bool) -> Class -> Bool
@@ -1665,7 +1681,7 @@ efoldReft logicBind cb dty g f fp = go
     go γ z (RAllP p t)                  = go (fp p γ) z t
     go γ z (RImpF x t t' r)             = go γ z (RFun x t t' r)
     go γ z me@(RFun _ (RApp c ts _ _) t' r)
-       | isClass c                      = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t')
+       | isEmbeddedDict c                      = f γ (Just me) r (go (insertsSEnv γ (cb c ts)) (go' γ z ts) t')
     go γ z me@(RFun x t t' r)
        | logicBind x t                  = f γ (Just me) r (go γ' (go γ z t) t')
        | otherwise                      = f γ (Just me) r (go γ  (go γ z t) t')