Typeclass with minor fixes

liquidhaskell.cabal

@@ -90,6 +90,7 @@ library
                       Language.Haskell.Liquid.Bare.Resolve
                       Language.Haskell.Liquid.Bare.ToBare
                       Language.Haskell.Liquid.Bare.Types
+                      Language.Haskell.Liquid.Bare.Elaborate
                       Language.Haskell.Liquid.Constraint.Constraint
                       Language.Haskell.Liquid.Constraint.Env
                       Language.Haskell.Liquid.Constraint.Fresh
@@ -123,6 +124,7 @@ library
                       Language.Haskell.Liquid.Transforms.ANF
                       Language.Haskell.Liquid.Transforms.CoreToLogic
                       Language.Haskell.Liquid.Transforms.Rec
+                      Language.Haskell.Liquid.Transforms.InlineAux
                       Language.Haskell.Liquid.Transforms.RefSplit
                       Language.Haskell.Liquid.Transforms.Rewrite
                       Language.Haskell.Liquid.Transforms.Simplify
@@ -190,6 +192,8 @@ library
                     , transformers         >= 0.3
                     , unordered-containers >= 0.2
                     , vector               >= 0.10
+                    , free
+                    , recursion-schemes
   default-language:   Haskell98
   default-extensions: PatternGuards
   ghc-options:        -W -fwarn-missing-signatures

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

@@ -54,9 +54,9 @@ 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
-                   then (x, val <$> lookup v sigs, v, e)
+findVarDefType cbs sigs x = case findVarDefMethod (val x) cbs of
+  Just (v, e) -> if Ghc.isExportedId v || isMethod (F.symbol x) || isDictionary (F.symbol x)
+                   then (F.notracepp "FIND-VAR-DEF-NAME" $ x, F.notracepp "FIND-VAR-DEF" $ 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"
 
@@ -106,7 +106,7 @@ 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 tx t) e | Ghc.isClassPred tx 
+grabBody (Ghc.FunTy tx t) e | isEmbeddedDictType tx
   = grabBody t e 
 grabBody (Ghc.FunTy _ t) (Ghc.Lam x e) 
   = (x:xs, e') where (xs, e') = grabBody t e
@@ -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/Bare/Check.hs

@@ -309,7 +309,7 @@ checkTerminationExpr emb env (v, Loc l _ t, les)
     xts     = concatMap mkClass $ zip (ty_binds trep) (ty_args trep)
     trep    = toRTypeRep t
 
-    mkClass (_, RApp c ts _ _) | isClass c = classBinds emb (rRCls c ts)
+    mkClass (_, RApp c ts _ _) | isEmbeddedDict c = classBinds emb (rRCls c ts)
     mkClass (x, t)                         = [(x, rSort t)]
 
     rSort   = rTypeSortedReft emb

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

@@ -114,7 +114,6 @@ addCC x zz@(Loc l l' st0)
     addForall _ t 
       = t 
 
-
 splitDictionary :: Ghc.CoreExpr -> Maybe (Ghc.Var, [Ghc.Type], [Ghc.Var])
 splitDictionary = go [] [] 
   where 
@@ -273,4 +272,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)