Flagged tc

liquidhaskell.cabal

@@ -91,6 +91,8 @@ library
                       Language.Haskell.Liquid.Bare.Resolve
                       Language.Haskell.Liquid.Bare.ToBare
                       Language.Haskell.Liquid.Bare.Types
+                      Language.Haskell.Liquid.Bare.Typeclass
+                      Language.Haskell.Liquid.Bare.Elaborate
                       Language.Haskell.Liquid.Constraint.Constraint
                       Language.Haskell.Liquid.Constraint.Env
                       Language.Haskell.Liquid.Constraint.Fresh
@@ -127,6 +129,7 @@ library
                       Language.Haskell.Liquid.Transforms.RefSplit
                       Language.Haskell.Liquid.Transforms.Rewrite
                       Language.Haskell.Liquid.Transforms.Simplify
+                      Language.Haskell.Liquid.Transforms.InlineAux
                       Language.Haskell.Liquid.Types
                       Language.Haskell.Liquid.Types.Bounds
                       Language.Haskell.Liquid.Types.Dictionaries
@@ -193,6 +196,8 @@ library
                     , transformers         >= 0.3
                     , unordered-containers >= 0.2
                     , vector               >= 0.10
+                    , recursion-schemes
+                    , free
   default-language:   Haskell98
   default-extensions: PatternGuards
   ghc-options:        -W -fwarn-missing-signatures

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

@@ -54,8 +54,10 @@ getReflectDefs src sig spec = findVarDefType cbs sigs <$> xs
 
 findVarDefType :: [Ghc.CoreBind] -> [(Ghc.Var, LocSpecType)] -> LocSymbol
                -> (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)
-findVarDefType cbs sigs x = case findVarDef (val x) cbs of
-  Just (v, e) -> if Ghc.isExportedId v
+findVarDefType cbs sigs x = case findVarDefMethod (val x) cbs of
+  -- YL: probably ok even without checking typeclass flag since user cannot
+  -- manually reflect internal names
+  Just (v, e) -> if Ghc.isExportedId v || isMethod (F.symbol x) || isDictionary (F.symbol x)
                    then (x, val <$> lookup v sigs, v, e)
                    else Ex.throw $ mkError x ("Lifted functions must be exported; please export " ++ show v)
   Nothing     -> Ex.throw $ mkError x "Cannot lift haskell function"
@@ -69,55 +71,60 @@ makeAxiom env tycEnv name lmap (x, mbT, v, def)
             = (v, t, e)
   where 
     t       = Bare.qualifyTop env name (F.loc t0) t0 
-    (t0, e) = makeAssumeType embs lmap dm x mbT v def
+    (t0, e) = makeAssumeType allowTC embs lmap dm x mbT v def
     embs    = Bare.tcEmbs       tycEnv 
-    dm      = Bare.tcDataConMap tycEnv 
+    dm      = Bare.tcDataConMap tycEnv
+    allowTC = typeclass (getConfig env)
 
 mkError :: LocSymbol -> String -> Error
 mkError x str = ErrHMeas (sourcePosSrcSpan $ loc x) (pprint $ val x) (PJ.text str)
 
 makeAssumeType
-  :: F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
+  :: Bool -- ^ typeclass enabled
+  -> F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
   -> Ghc.Var -> Ghc.CoreExpr
   -> (LocSpecType, F.Equation)
-makeAssumeType tce lmap dm x mbT v def
+makeAssumeType allowTC tce lmap dm x mbT v def
   = (x {val = aty at `strengthenRes` F.subst su ref},  F.mkEquation (val x) xts (F.subst su le) out)
   where
     t     = Mb.fromMaybe (ofType τ) mbT
     τ     = Ghc.varType v
-    at    = axiomType x t
+    at    = axiomType allowTC x t
     out   = rTypeSort tce $ ares at 
     xArgs = (F.EVar . fst) <$> aargs at
     _msg  = unwords [showpp x, showpp mbT]
-    le    = case runToLogicWithBoolBinds bbs tce lmap dm mkErr (coreToLogic  def') of
+    le    = case runToLogicWithBoolBinds bbs tce lmap dm mkErr (coreToLogic allowTC def') of
               Right e -> e
               Left  e -> panic Nothing (show e)
     ref        = F.Reft (F.vv_, F.PAtom F.Eq (F.EVar F.vv_) le)
     mkErr s    = ErrHMeas (sourcePosSrcSpan $ loc x) (pprint $ val x) (PJ.text s)
     bbs        = filter isBoolBind xs
-    (xs, def') = grabBody (Ghc.expandTypeSynonyms τ) $ normalize def
+    (xs, def') = grabBody allowTC (Ghc.expandTypeSynonyms τ) $ normalize allowTC def
     su         = F.mkSubst  $ zip (F.symbol     <$> xs) xArgs
                            ++ zip (simplesymbol <$> xs) xArgs
     xts        = [(F.symbol x, rTypeSortExp tce t) | (x, t) <- aargs at]
 
 rTypeSortExp :: F.TCEmb Ghc.TyCon -> SpecType -> F.Sort
 rTypeSortExp tce = typeSort tce . Ghc.expandTypeSynonyms . toType
 
-grabBody :: Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr)
-grabBody (Ghc.ForAllTy _ t) e 
-  = grabBody t e 
-grabBody (Ghc.FunTy { Ghc.ft_arg = tx, Ghc.ft_res = t}) e | Ghc.isClassPred tx 
-  = grabBody t e 
-grabBody (Ghc.FunTy { Ghc.ft_res = t}) (Ghc.Lam x e) 
-  = (x:xs, e') where (xs, e') = grabBody t e
-grabBody t (Ghc.Tick _ e) 
-  = grabBody t e
-grabBody t@(Ghc.FunTy {}) e               
+grabBody :: Bool -- ^ typeclass enabled
+         -> Ghc.Type -> Ghc.CoreExpr -> ([Ghc.Var], Ghc.CoreExpr)
+grabBody allowTC (Ghc.ForAllTy _ t) e 
+  = grabBody allowTC t e 
+grabBody allowTC@False (Ghc.FunTy { Ghc.ft_arg = tx, Ghc.ft_res = t}) e | Ghc.isClassPred tx 
+  = grabBody allowTC t e 
+grabBody allowTC@True (Ghc.FunTy { Ghc.ft_arg = tx, Ghc.ft_res = t}) e | isEmbeddedDictType tx 
+  = grabBody allowTC t e 
+grabBody allowTC (Ghc.FunTy { Ghc.ft_res = t}) (Ghc.Lam x e) 
+  = (x:xs, e') where (xs, e') = grabBody allowTC t e
+grabBody allowTC t (Ghc.Tick _ e) 
+  = grabBody allowTC t e
+grabBody allowTC t@(Ghc.FunTy {}) e               
   = (txs++xs, e') 
    where (ts,tr)  = splitFun t 
-         (xs, e') = grabBody tr (foldl Ghc.App e (Ghc.Var <$> txs))
+         (xs, e') = grabBody allowTC tr (foldl Ghc.App e (Ghc.Var <$> txs))
          txs      = [ stringVar ("ls" ++ show i) t |  (t,i) <- zip ts [1..]]
-grabBody _ e              
+grabBody allowTC _ e              
   = ([], e)
 
 splitFun :: Ghc.Type -> ([Ghc.Type], Ghc.Type)
@@ -172,13 +179,13 @@ instance Subable Ghc.CoreAlt where
 data AxiomType = AT { aty :: SpecType, aargs :: [(F.Symbol, SpecType)], ares :: SpecType }
 
 -- | Specification for Haskell function
-axiomType :: LocSymbol -> SpecType -> AxiomType
-axiomType s t = AT to (reverse xts) res  
+axiomType :: Bool -> LocSymbol -> SpecType -> AxiomType
+axiomType allowTC s t = AT to (reverse xts) res  
   where
     (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) | isErasable 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 
@@ -191,7 +198,7 @@ axiomType s t = AT to (reverse xts) res
       let t' = strengthen t (singletonApp s ys)
       put (i, bs, Just t')
       return t' 
-
+    isErasable = if allowTC then isEmbeddedClass else isClassType
 unDummy :: F.Symbol -> Int -> F.Symbol
 unDummy x i
   | x /= F.dummySymbol = x

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

@@ -106,15 +106,15 @@ checkTargetSpec :: [Ms.BareSpec]
                 -> Either [Error] TargetSpec
 checkTargetSpec specs src env cbs sp = Misc.applyNonNull (Right sp) Left errors
   where
-    errors           =  mapMaybe (checkBind allowHO bsc "measure"      emb tcEnv env) (gsMeas       (gsData sp))
+    errors           =  mapMaybe (checkBind allowTC allowHO bsc "measure"      emb tcEnv env) (gsMeas       (gsData sp))
                      ++ condNull noPrune 
-                        (mapMaybe (checkBind allowHO bsc "constructor"  emb tcEnv env) (txCtors $ gsCtors      (gsData sp)))
-                     ++ mapMaybe (checkBind allowHO bsc "assume"       emb tcEnv env) (gsAsmSigs    (gsSig sp))
-                     ++ checkTySigs         allowHO bsc cbs            emb tcEnv env                (gsSig sp)
+                        (mapMaybe (checkBind allowTC allowHO bsc "constructor"  emb tcEnv env) (txCtors $ gsCtors      (gsData sp)))
+                     ++ mapMaybe (checkBind allowTC allowHO bsc "assume"       emb tcEnv env) (gsAsmSigs    (gsSig sp))
+                     ++ checkTySigs         allowTC allowHO bsc cbs            emb tcEnv env                (gsSig sp)
                      -- ++ mapMaybe (checkTerminationExpr             emb       env) (gsTexprs     (gsSig  sp)) 
-                     ++ mapMaybe (checkBind allowHO bsc "class method" emb tcEnv env) (clsSigs      (gsSig sp))
-                     ++ mapMaybe (checkInv allowHO bsc emb tcEnv env)                 (gsInvariants (gsData sp))
-                     ++ checkIAl allowHO bsc emb tcEnv env                            (gsIaliases   (gsData sp))
+                     ++ mapMaybe (checkBind allowTC allowHO bsc "class method" emb tcEnv env) (clsSigs      (gsSig sp))
+                     ++ mapMaybe (checkInv allowTC allowHO bsc emb tcEnv env)                 (gsInvariants (gsData sp))
+                     ++ checkIAl allowTC allowHO bsc emb tcEnv env                            (gsIaliases   (gsData sp))
                      ++ checkMeasures emb env ms
                      ++ checkClassMeasures                                        (gsMeasures (gsData sp))
                      ++ checkClassMethods (gsCls src) (gsCMethods (gsVars sp)) (gsTySigs     (gsSig sp))
@@ -143,6 +143,7 @@ checkTargetSpec specs src env cbs sp = Misc.applyNonNull (Right sp) Left errors
     ms               = gsMeasures (gsData sp)
     clsSigs sp       = [ (v, t) | (v, t) <- gsTySigs sp, isJust (isClassOpId_maybe v) ]
     sigs             = gsTySigs (gsSig sp) ++ gsAsmSigs (gsSig sp) ++ gsCtors (gsData sp)
+    allowTC          = typeclass (getConfig sp)
     allowHO          = higherOrderFlag sp
     bsc              = bscope (getConfig sp)
     noPrune          = not (pruneFlag sp)
@@ -162,17 +163,17 @@ checkPlugged xs = mkErr <$> filter (hasHoleTy . val . snd) xs
 
 
 --------------------------------------------------------------------------------
-checkTySigs :: Bool -> BScope -> [CoreBind] -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
+checkTySigs :: Bool -> Bool -> BScope -> [CoreBind] -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
             -> GhcSpecSig
             -> [Error]
 --------------------------------------------------------------------------------
-checkTySigs allowHO bsc cbs emb tcEnv env sig
+checkTySigs allowTC allowHO bsc cbs emb tcEnv env sig
                    = concatMap (check env) topTs
                    -- (mapMaybe   (checkT env) [ (x, t)     | (x, (t, _)) <- topTs])
                    -- ++ (mapMaybe   (checkE env) [ (x, t, es) | (x, (t, Just es)) <- topTs]) 
                    ++ coreVisitor checkVisitor env [] cbs 
   where 
-    check env      = checkSigTExpr allowHO bsc emb tcEnv env
+    check env      = checkSigTExpr allowTC allowHO bsc emb tcEnv env
     locTm          = M.fromList locTs
     (locTs, topTs) = Bare.partitionLocalBinds vtes 
     vtes           = [ (x, (t, es)) | (x, t) <- gsTySigs sig, let es = M.lookup x vExprs]
@@ -189,13 +190,13 @@ checkTySigs allowHO bsc cbs emb tcEnv env sig
                          Nothing -> [] 
                          Just t  -> check env (v, t) 
 
-checkSigTExpr :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
+checkSigTExpr :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft 
               -> (Var, (LocSpecType, Maybe [Located F.Expr])) 
               -> [Error]
-checkSigTExpr allowHO bsc emb tcEnv env (x, (t, es)) 
+checkSigTExpr allowTC allowHO bsc emb tcEnv env (x, (t, es)) 
            = catMaybes [mbErr1, mbErr2] 
    where 
-    mbErr1 = checkBind allowHO bsc empty emb tcEnv env (x, t) 
+    mbErr1 = checkBind allowTC allowHO bsc empty emb tcEnv env (x, t) 
     mbErr2 = checkTerminationExpr emb env . (x, t,) =<< es 
 
 _checkQualifiers :: F.SEnv F.SortedReft -> [F.Qualifier] -> [Error]
@@ -263,24 +264,25 @@ _firstDuplicate = go . L.sort
                 | otherwise = go (x:xs)
     go _                    = Nothing
 
-checkInv :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Maybe Var, LocSpecType) -> Maybe Error
-checkInv allowHO bsc emb tcEnv env (_, t) = checkTy allowHO bsc err emb tcEnv env t
+checkInv :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (Maybe Var, LocSpecType) -> Maybe Error
+checkInv allowTC allowHO bsc emb tcEnv env (_, t) = checkTy allowTC allowHO bsc err emb tcEnv env t
   where
     err              = ErrInvt (GM.sourcePosSrcSpan $ loc t) (val t)
 
-checkIAl :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> [(LocSpecType, LocSpecType)] -> [Error]
-checkIAl allowHO bsc emb tcEnv env ials = catMaybes $ concatMap (checkIAlOne allowHO bsc emb tcEnv env) ials
+checkIAl :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> [(LocSpecType, LocSpecType)] -> [Error]
+checkIAl allowTC allowHO bsc emb tcEnv env ials = catMaybes $ concatMap (checkIAlOne allowTC allowHO bsc emb tcEnv env) ials
 
 checkIAlOne :: Bool
+            -> Bool
             -> BScope
             -> F.TCEmb TyCon
             -> Bare.TyConMap
             -> F.SEnv F.SortedReft
             -> (LocSpecType, LocSpecType)
             -> [Maybe (TError SpecType)]
-checkIAlOne allowHO bsc emb tcEnv env (t1, t2) = checkEq : (tcheck <$> [t1, t2])
+checkIAlOne allowTC allowHO bsc emb tcEnv env (t1, t2) = checkEq : (tcheck <$> [t1, t2])
   where
-    tcheck t = checkTy allowHO bsc (err t) emb tcEnv env t
+    tcheck t = checkTy allowTC allowHO bsc (err t) emb tcEnv env t
     err    t = ErrIAl (GM.sourcePosSrcSpan $ loc t) (val t)
     t1'      :: RSort
     t1'      = toRSort $ val t1
@@ -297,8 +299,8 @@ checkRTAliases msg _ as = err1s
   where
     err1s               = checkDuplicateRTAlias msg as
 
-checkBind :: (PPrint v) => Bool -> BScope -> Doc -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (v, LocSpecType) -> Maybe Error
-checkBind allowHO bsc s emb tcEnv env (v, t) = checkTy allowHO bsc msg emb tcEnv env t
+checkBind :: (PPrint v) => Bool -> Bool -> BScope -> Doc -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> (v, LocSpecType) -> Maybe Error
+checkBind allowTC allowHO bsc s emb tcEnv env (v, t) = checkTy allowTC allowHO bsc msg emb tcEnv env t
   where
     msg                      = ErrTySpec (GM.fSrcSpan t) (Just s) (pprint v) (val t)
 
@@ -324,8 +326,8 @@ checkTerminationExpr emb env (v, Loc l _ t, les)
     rSort   = rTypeSortedReft emb
     cmpZero e = F.PAtom F.Le (F.expr (0 :: Int)) (val e)
 
-checkTy :: Bool -> BScope -> (Doc -> Error) -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Error
-checkTy allowHO bsc mkE emb tcEnv env t = mkE <$> checkRType allowHO bsc emb env (Bare.txRefSort tcEnv emb t)
+checkTy :: Bool -> Bool -> BScope -> (Doc -> Error) -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Error
+checkTy allowTC allowHO bsc mkE emb tcEnv env t = mkE <$> checkRType allowTC allowHO bsc emb env (Bare.txRefSort tcEnv emb t)
   where
     _msg =  "CHECKTY: " ++ showpp (val t)
 
@@ -393,13 +395,14 @@ errTypeMismatch x t = ErrMismatch lqSp (pprint x) (text "Checked")  d1 d2 Nothin
 ------------------------------------------------------------------------------------------------
 -- | @checkRType@ determines if a type is malformed in a given environment ---------------------
 ------------------------------------------------------------------------------------------------
-checkRType :: Bool -> BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Doc
+checkRType :: Bool -> Bool -> BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Doc
 ------------------------------------------------------------------------------------------------
-checkRType allowHO bsc emb env lt
+checkRType allowTC allowHO bsc emb env lt
   =   checkAppTys t
   <|> checkAbstractRefs t
-  <|> efoldReft farg bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv env Nothing t
+  <|> efoldReft isErasable farg bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv env Nothing t
   where
+    isErasable         = if allowTC then isEmbeddedDict else isClass
     t                  = val lt
     cb c ts            = classBinds emb (rRCls c ts)
     farg _ t           = allowHO || isBase t  -- NOTE: this check should be the same as the one in addCGEnv
@@ -547,7 +550,7 @@ checkMBody γ emb _ sort (Def m c _ bs body) = checkMBody' emb sort γ' sp body
   where
     sp    = F.srcSpan m
     γ'    = L.foldl' (\γ (x, t) -> F.insertSEnv x t γ) γ xts
-    xts   = zip (fst <$> bs) $ rTypeSortedReft emb . subsTyVars_meet su <$> filter (not . isClassType) (ty_args trep)
+    xts   = zip (fst <$> bs) $ rTypeSortedReft emb . subsTyVars_meet su <$>  (ty_args trep)
     trep  = toRTypeRep ct
     su    = checkMBodyUnify (ty_res trep) (last txs)
     txs   = snd4 $ bkArrowDeep sort

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

@@ -41,10 +41,10 @@ import qualified Control.Exception                 as Ex
 
 
 -------------------------------------------------------------------------------
-makeMethodTypes :: DEnv Ghc.Var LocSpecType -> [DataConP] -> [Ghc.CoreBind] -> [(Ghc.Var, MethodType LocSpecType)]
+makeMethodTypes :: Bool -> DEnv Ghc.Var LocSpecType -> [DataConP] -> [Ghc.CoreBind] -> [(Ghc.Var, MethodType LocSpecType)]
 -------------------------------------------------------------------------------
-makeMethodTypes (DEnv m) cls cbs 
-  = [(x, MT (addCC x . fromRISig <$> methodType d x m) (addCC x <$> classType (splitDictionary e) x)) | (d,e) <- ds, x <- grepMethods e]
+makeMethodTypes allowTC (DEnv m) cls cbs 
+  = [(x, MT (addCC allowTC x . fromRISig <$> methodType d x m) (addCC allowTC x <$> classType (splitDictionary e) x)) | (d,e) <- ds, x <- grepMethods e]
     where 
       grepMethods = filter GM.isMethod . freeVars mempty
       ds = filter (GM.isDictionary . fst) (concatMap unRec cbs)
@@ -67,8 +67,8 @@ makeMethodTypes (DEnv m) cls cbs
       subst [] t = t 
       subst ((a,ta):su) t = subsTyVar_meet' (a,ofType ta) (subst su t)
 
-addCC :: Ghc.Var -> LocSpecType -> LocSpecType
-addCC x zz@(Loc l l' st0) 
+addCC :: Bool -> Ghc.Var -> LocSpecType -> LocSpecType
+addCC allowTC x zz@(Loc l l' st0) 
   = Loc l l' 
   . addForall hst  
   . mkArrow [] ps' [] [] 
@@ -79,7 +79,7 @@ addCC x zz@(Loc l l' st0)
   where
     hst           = ofType (Ghc.expandTypeSynonyms t0) :: SpecType
     t0            = Ghc.varType x 
-    tyvsmap       = case Bare.runMapTyVars t0 st err of
+    tyvsmap       = case Bare.runMapTyVars allowTC t0 st err of
                           Left e  -> Ex.throw e 
                           Right s -> Bare.vmap s
     su            = [(y, rTyVar x)           | (x, y) <- tyvsmap]
@@ -273,4 +273,4 @@ lookupDefaultVar env name v = Mb.maybeToList
   where 
     dmSym                   = F.atLoc v (GM.qualifySymbol mSym dnSym)
     dnSym                   = F.mappendSym "$dm" nSym
-    (mSym, nSym)            = GM.splitModuleName (F.symbol v) 
+    (mSym, nSym)            = GM.splitModuleName (F.symbol v)