PGF.Type.Hypo now can represent explicit and implicit arguments and argument without bound variable

src/PGF/Binary.hs

@@ -146,8 +146,14 @@ instance Binary Type where
   get = liftM3 DTyp get get get
 
 instance Binary Hypo where
-  put (Hyp v t) = put (v,t)
-  get = liftM2 Hyp get get
+  put (Hyp    t) = putWord8 0 >> put t
+  put (HypV v t) = putWord8 1 >> put (v,t)
+  put (HypI v t) = putWord8 2 >> put (v,t)
+  get = do tag <- getWord8
+           case tag of
+             0 -> liftM  Hyp  get 
+             1 -> liftM2 HypV get get
+             2 -> liftM2 HypI get get
 
 instance Binary FFun where
   put (FFun fun prof lins) = put (fun,prof,lins)

src/PGF/Macros.hs

@@ -105,15 +105,20 @@ depth (Fun _ ts) = maximum (0:map depth ts) + 1
 depth _          = 1
 
 cftype :: [CId] -> CId -> Type
-cftype args val = DTyp [Hyp wildCId (cftype [] arg) | arg <- args] val []
+cftype args val = DTyp [Hyp (cftype [] arg) | arg <- args] val []
+
+typeOfHypo :: Hypo -> Type
+typeOfHypo (Hyp    ty) = ty
+typeOfHypo (HypV _ ty) = ty
+typeOfHypo (HypI _ ty) = ty
 
 catSkeleton :: Type -> ([CId],CId)
 catSkeleton ty = case ty of
-  DTyp hyps val _ -> ([valCat ty | Hyp _ ty <- hyps],val)
+  DTyp hyps val _ -> ([valCat (typeOfHypo h) | h <- hyps],val)
 
 typeSkeleton :: Type -> ([(Int,CId)],CId)
 typeSkeleton ty = case ty of
-  DTyp hyps val _ -> ([(contextLength ty, valCat ty) | Hyp _ ty <- hyps],val)
+  DTyp hyps val _ -> ([(contextLength ty, valCat ty) | h <- hyps, let ty = typeOfHypo h],val)
 
 valCat :: Type -> CId
 valCat ty = case ty of

src/PGF/Type.hs

@@ -15,9 +15,12 @@ data Type =
    DTyp [Hypo] CId [Expr]
   deriving (Eq,Ord)
 
+-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis
 data Hypo =
-   Hyp CId Type
-  deriving (Eq,Ord,Show)
+    Hyp      Type      -- ^ hypothesis without bound variable like in A -> B
+  | HypV CId Type      -- ^ hypothesis with bound variable like in (x : A) -> B x
+  | HypI CId Type      -- ^ hypothesis with bound implicit variable like in {x : A} -> B x
+  deriving (Eq,Ord)
 
 -- | Reads a 'Type' from a 'String'.
 readType :: String -> Maybe Type
@@ -45,7 +48,7 @@ pType = do
   where
     pHypo =
       do (cat,args) <- pAtom
-         return (Hyp wildCId (DTyp [] cat args))
+         return (Hyp (DTyp [] cat args))
       RP.<++
       (RP.between (RP.char '(') (RP.char ')') $ do
          var <- RP.option wildCId $ do
@@ -54,7 +57,16 @@ pType = do
                      RP.string ":"
                      return v
          ty <- pType
-         return (Hyp var ty))
+         return (HypV var ty))
+      RP.<++
+      (RP.between (RP.char '{') (RP.char '}') $ do
+         var <- RP.option wildCId $ do
+                     v <- pCId
+                     RP.skipSpaces
+                     RP.string ":"
+                     return v
+         ty <- pType
+         return (HypI var ty))
 
     pAtom = do
       cat <- pCId
@@ -70,9 +82,9 @@ ppType d (DTyp ctxt cat args)
     ppCtxt hyp doc = ppHypo hyp PP.<+> PP.text "->" PP.<+> doc
     ppRes cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 2) es)
 
-ppHypo (Hyp x typ)
-  | x == wildCId = ppType 1 typ
-  | otherwise    = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
+ppHypo (Hyp    typ) = ppType 1 typ
+ppHypo (HypV x typ) = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
+ppHypo (HypI x typ) = PP.braces (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
 
 ppParens :: Bool -> PP.Doc -> PP.Doc
 ppParens True  = PP.parens

src/PGF/TypeCheck.hs

@@ -91,7 +91,10 @@ lookupEVar pgf (_,g,_) x = case Map.lookup x g of
 
 type2expr :: Type -> Expr
 type2expr (DTyp hyps cat es) = 
-  foldr (uncurry EPi) (foldl EApp (EVar cat) es) [(x, type2expr t) | Hyp x t <- hyps]
+  foldr (uncurry EPi) (foldl EApp (EVar cat) es) [toPair h | h <- hyps]
+  where
+    toPair (Hyp    t) = (wildCId, type2expr t)
+    toPair (HypV x t) = (x,       type2expr t)
 
 type TCEnv = (Int,Env,Env)
 
@@ -156,7 +159,7 @@ splitConstraints pgf = mkSplit . unifyAll [] . map reduce where
     (VMeta s _, t) -> do
       let tg = substMetas g t
       let sg = maybe e1 id (lookup s g)
-      if (sg == e1) then extend s tg g else unify sg tg g 
+      if null (eqValue (funs (abstract pgf)) 0 sg e1) then extend s tg g else unify sg tg g 
     (t, VMeta _ _) -> unify e2 e1 g
     (VApp c as, VApp d bs) | c == d -> 
        foldM (\ h (a,b) -> unify a b h) g (zip as bs)