[drop quantified variables from ForallT constructor
Helmut Grohne <grohne@cs.uni-bonn.de>**20150312121258
 Ignore-this: 9834dc0b1822eef8bf61b20c5089f660
 
 Unless enabling RankNTypes (which Igor doesn't do), forall can only occur
 outermost and all free variables in the type are automatically quantified. Thus
 the quantified variables can easily be determined by looking at the Type
 parameter of ForallT. In fact, the only place where this parameter is used
 (besides fixType and quantify) is the pretty printer.
] hunk ./src/Igor2/Config.hs 64
-    [('(==), forallT ["a"] [(''Eq, "a")] $ arrowT [varT "a", varT "a", boolCon])
---    , '(/=), forallT ["a"] [(''Eq, "a")] $ arrowT [varT "a", varT "a", boolCon])
-    ,('(<), forallT ["a"] [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
---    ,('(>=), forallT ["a"] [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
-    ,('(>), forallT ["a"] [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
---    ,('(<=), forallT ["a"] [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
+    [('(==), forallT [(''Eq, "a")] $ arrowT [varT "a", varT "a", boolCon])
+--    , '(/=), forallT [(''Eq, "a")] $ arrowT [varT "a", varT "a", boolCon])
+    ,('(<), forallT [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
+--    ,('(>=), forallT [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
+    ,('(>), forallT [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
+--    ,('(<=), forallT [(''Ord, "a")] $ arrowT [varT "a", varT "a", boolCon])
hunk ./src/Igor2/RuleDevelopment/Cata.hs 210
-muVar = tVarE "a" $ forallT ["a"][ (''Mu,"a")] (varT "a")
-funcVar = tVarE "a" $ forallT ["a"][ (''Functor,"a")] (varT "a")
+muVar = tVarE "a" $ forallT [(''Mu, "a")] (varT "a")
+funcVar = tVarE "a" $ forallT [(''Functor, "a")] (varT "a")
hunk ./src/Igor2/RuleDevelopment/Cata.hs 216
-         ForallT [ mkName "a", mkName "b"]
-                 [ mkPred ''Mu "a"
+         ForallT [ mkPred ''Mu "a"
hunk ./src/Igor2/RuleDevelopment/Cata.hs 221
-         ForallT [ mkName "a", mkName "b"]
-                 [ mkPred ''Mu "a"
+         ForallT [ mkPred ''Mu "a"
hunk ./src/Syntax/Builder.hs 160
-mkForallT assts ty   = 
-    fixType $ ForallT [] (getPreds assts) ty             
+mkForallT assts ty   =
+    fixType $ ForallT (getPreds assts) ty
hunk ./src/Syntax/Builder.hs 393
-  toType (Hs.TyForall Nothing x t) = fixType $ ForallT [] (getPreds x)(toType t)
+  toType (Hs.TyForall Nothing x t) = fixType $ ForallT (getPreds x) (toType t)
hunk ./src/Syntax/Context.hs 129
-    ,('undefined, forallT ["a"] [] (varT "a"))
+    ,('undefined, varT "a")
hunk ./src/Syntax/Context.hs 160
-            , forallT ["a"][(''Eq,"a")] $ listT (varT "a")
-            , forallT ["a"][(''Eq,"a")] $ appT maybeCon (varT "a")
+            , forallT [(''Eq, "a")] $ listT (varT "a")
+            , forallT [(''Eq, "a")] $ appT maybeCon (varT "a")
hunk ./src/Syntax/Context.hs 165
-             , forallT ["a"][(''Ord,"a")] $ listT (varT "a")
-             , forallT ["a"][(''Ord,"a")] $ appT maybeCon (varT "a")
+             , forallT [(''Ord, "a")] $ listT (varT "a")
+             , forallT [(''Ord, "a")] $ appT maybeCon (varT "a")
hunk ./src/Syntax/Ppr.hs 57
-    pretty (ForallT tvars ctxt ty) = 
-            text "forall" <+> hsep (map pretty tvars) <+> text "."
+    pretty (ForallT ctxt ty) =
+            text "forall" <+> hsep (map pretty (getVarNames ty)) <+> text "."
hunk ./src/Syntax/Type.hs 59
-data Type = ForallT [Name] TyCxt Type
+data Type = ForallT TyCxt Type
hunk ./src/Syntax/Type.hs 92
-dataName (ForallT _ _ t) = dataName t
-dataName (VarT _)        = throwError . strMsg $ "dataName: Variable!"
-dataName (ConT n)        = return n
-dataName (AppT t _)      = dataName t
+dataName (ForallT _ t) = dataName t
+dataName (VarT _)      = throwError . strMsg $ "dataName: Variable!"
+dataName (ConT n)      = return n
+dataName (AppT t _)    = dataName t
hunk ./src/Syntax/Type.hs 130
-unArrowT (ForallT ns cxt t) = map (flip quantify cxt) $ unArrowT t
+unArrowT (ForallT cxt t) = map (flip quantify cxt) $ unArrowT t
hunk ./src/Syntax/Type.hs 141
-forallT :: [String] -> [(Name, String)] -> Type -> Type
-forallT vs ps t = fixType $ ForallT (map mkName vs) (map (uncurry mkPred) ps) t
+forallT :: [(Name, String)] -> Type -> Type
+forallT ps t = fixType $ ForallT (map (uncurry mkPred) ps) t
hunk ./src/Syntax/Type.hs 159
-appT (ForallT _ c1 t1)(ForallT _ c2 t2) = quantify (AppT t1 t2) (c1++c2)
-appT  t1              (ForallT _ c t2)  = quantify (AppT t1 t2) c
-appT (ForallT _ c t1)  t2               = quantify (AppT t1 t2) c
-appT  t1               t2               = AppT t1 t2
+appT (ForallT c1 t1) (ForallT c2 t2) = quantify (AppT t1 t2) (c1 ++ c2)
+appT  t1             (ForallT c t2)  = quantify (AppT t1 t2) c
+appT (ForallT c t1)  t2              = quantify (AppT t1 t2) c
+appT  t1             t2              = AppT t1 t2
hunk ./src/Syntax/Type.hs 171
-    where 
-    f done (ForallT ns cxt t) = map (flip quantify cxt) $ f done t
-    f done (AppT e1 e2)       = f (e2:done) e1
-    f done e                  = e:done
+    where
+    f done (ForallT cxt t) = map (flip quantify cxt) $ f done t
+    f done (AppT e1 e2)    = f (e2:done) e1
+    f done e               = e:done
hunk ./src/Syntax/Type.hs 177
-fixType (ForallT ns cxt t) 
-    | null cxt  = t
-    | null ns   = quantify t cxt
-    | otherwise = (ForallT (nub ns) cxt t) 
+fixType (ForallT cxt t) = quantify t cxt
hunk ./src/Syntax/Type.hs 192
-    
-    sameSymAtRoot (ForallT _ c1 t1)(ForallT _ c2 t2) = (sameSymAtRoot t1 t2) && ((c1 `intersect` c2) == c1) 
---    sameSymAtRoot (ForallT _ c1 t1) t2        = sameSymAtRoot t1 t2 
---    sameSymAtRoot t1 (ForallT _ _ t2)         = sameSymAtRoot t1 t2
-    sameSymAtRoot t1@(AppT _ _) t2@(AppT _ _) = on (==) (head.unfoldAppT) t1 t2
+
+    sameSymAtRoot (ForallT c1 t1) (ForallT c2 t2) = sameSymAtRoot t1 t2 && ((c1 `intersect` c2) == c1)
+--    sameSymAtRoot (ForallT c1 t1) t2          = sameSymAtRoot t1 t2
+--    sameSymAtRoot t1 (ForallT _ t2)           = sameSymAtRoot t1 t2
+    sameSymAtRoot t1@(AppT _ _) t2@(AppT _ _) = on (==) (head . unfoldAppT) t1 t2
hunk ./src/Syntax/Type.hs 198
-        
-    subterms (ForallT _ c t) = map (flip quantify c) (subterms t)
-    subterms (AppT l r)      = [l,r]
-    subterms _               = []
+
+    subterms (ForallT c t) = map (flip quantify c) (subterms t)
+    subterms (AppT l r)    = [l, r]
+    subterms _             = []
hunk ./src/Syntax/Type.hs 209
-    root (ForallT ns c t) = \ts -> quantify (root t (map rmCxt ts)) (nub $ concatMap tyCxt ts)
-    root (AppT _ _)       = \[l,r] -> appT l r
-    root t                = const t
-    
+    root (ForallT c t) = \ts -> quantify (root t (map rmCxt ts)) (nub $ concatMap tyCxt ts)
+    root (AppT _ _)    = \[l, r] -> appT l r
+    root t             = const t
+
hunk ./src/Syntax/Type.hs 223
-  apply s (VarT u)        = fromMaybe (VarT u) (lookupS u s)
-  apply s (AppT l r)      = appT (apply s l) (apply s r)
-  apply s (ForallT _ c t) = quantify (apply s t) c
-  apply s t         = t
-  
+  apply s (VarT u)      = fromMaybe (VarT u) (lookupS u s)
+  apply s (AppT l r)    = appT (apply s l) (apply s r)
+  apply s (ForallT c t) = quantify (apply s t) c
+  apply s t             = t
+
hunk ./src/Syntax/Type.hs 233
-quantify (ForallT ns cxt t) qtys = 
-    let ns'  = nub . (ns++) . (quantifiedVars t) $ qtys
-        cxt' = nub . (allPreds ns') . (cxt++) $ qtys
-    in if null cxt' then t else (ForallT ns' cxt' t)
+quantify (ForallT cxt t) qtys =
+    let cxt' = nub $ allPreds (getVarNames t) (cxt ++ qtys)
+    in if null cxt' then t else ForallT cxt' t
hunk ./src/Syntax/Type.hs 237
-    -- returns only those names of quantified type variables which actually
-    -- occur in both, the type and the context
-    quantifiedVars :: Type -> TyCxt -> [Name]
-    quantifiedVars t = intersect (getVarNames t) . concatMap (getVarNames . predMember)
-quantify t@(AppT _ _) qtys = quantify (ForallT [] [] t) qtys
-quantify t@(VarT _) qtys = quantify (ForallT [] [] t) qtys
+quantify t@(AppT _ _) qtys = quantify (ForallT [] t) qtys
+quantify t@(VarT _) qtys = quantify (ForallT [] t) qtys
hunk ./src/Syntax/Type.hs 243
-tyCxt (ForallT _ cxt _) = cxt
-tyCxt         _         = []
+tyCxt (ForallT cxt _) = cxt
+tyCxt        _        = []
hunk ./src/Syntax/Type.hs 247
-rmCxt (ForallT _ _ t) = t
-rmCxt         t       = t
+rmCxt (ForallT _ t) = t
+rmCxt        t      = t
hunk ./src/Syntax/Type.hs 251
-propCxt t@(ForallT _ _ (VarT _))  = t
-propCxt (ForallT _ cxt (AppT l r)) = AppT (quantify l cxt)(quantify r cxt)
+propCxt t@(ForallT _ (VarT _))   = t
+propCxt (ForallT cxt (AppT l r)) = AppT (quantify l cxt) (quantify r cxt)
hunk ./src/Syntax/UnifyTy.hs 43
-    match t (VarT n)                 = return $ n <~ t
-    match t (ForallT _ c (VarT n))   = check (n <~ t) c >> return (n <~ t)
-    match t (ForallT _ c (AppT l r)) = match t (AppT (quantify l c)(quantify r c))
-    match (ForallT _ c (AppT l r)) t = match (AppT (quantify l c)(quantify r c)) t
-    match (AppT l r)(AppT l' r')     = do sl <- match l l'
-                                          sr <- match r r'
-                                          merge sl sr
+    match t (VarT n)               = return $ n <~ t
+    match t (ForallT c (VarT n))   = check (n <~ t) c >> return (n <~ t)
+    match t (ForallT c (AppT l r)) = match t (AppT (quantify l c) (quantify r c))
+    match (ForallT c (AppT l r)) t = match (AppT (quantify l c) (quantify r c)) t
+    match (AppT l r) (AppT l' r')  = do sl <- match l l'
+                                        sr <- match r r'
+                                        merge sl sr
hunk ./src/Syntax/UnifyTy.hs 51
-        | n == n'                    = return nullSubst
-    match t1 t2                      = throwError . strMsg $ "Type " ++ show t1 ++
-                                              " does not match " ++ 
-                                              (show t2) ++ "."
+        | n == n'                  = return nullSubst
+    match t1 t2                    = throwError . strMsg $ "Type " ++ show t1 ++
+                                              " does not match " ++
+                                              show t2 ++ "."
hunk ./src/Syntax/UnifyTy.hs 56
-    mgu (VarT n) t                 = return $ n <~ t
-    mgu t (VarT n)                 = return $ n <~ t
-    mgu (ForallT _ c (VarT n)) t   = check (n <~ t) c >> return (n <~ t)
-    mgu t (ForallT _ c (VarT n))   = check (n <~ t) c >> return (n <~ t)
-    mgu (ForallT _ c (AppT l r)) t = mgu (AppT (quantify l c)(quantify r c)) t
-    mgu t (ForallT _ c (AppT l r)) = mgu t (AppT (quantify l c)(quantify r c))
-    mgu (AppT l r)(AppT l' r')     = do sl <- mgu l l'
-                                        sr <- mgu r r'
-                                        return $ sl @@ sr
+    mgu (VarT n) t               = return $ n <~ t
+    mgu t (VarT n)               = return $ n <~ t
+    mgu (ForallT c (VarT n)) t   = check (n <~ t) c >> return (n <~ t)
+    mgu t (ForallT c (VarT n))   = check (n <~ t) c >> return (n <~ t)
+    mgu (ForallT c (AppT l r)) t = mgu (AppT (quantify l c) (quantify r c)) t
+    mgu t (ForallT c (AppT l r)) = mgu t (AppT (quantify l c) (quantify r c))
+    mgu (AppT l r) (AppT l' r')  = do sl <- mgu l l'
+                                      sr <- mgu r r'
+                                      return $ sl @@ sr
hunk ./src/Syntax/UnifyTy.hs 66
-        | n == n'                  = return nullSubst
-    mgu t1 t2                      = throwError . strMsg $ "Type " ++ show t1 ++
+        | n == n'                = return nullSubst
+    mgu t1 t2                    = throwError . strMsg $ "Type " ++ show t1 ++
hunk ./src/Syntax/UnifyTy.hs 96
-satisfies t@(VarT _) p               = return True
+satisfies t@(VarT _) p             = return True
hunk ./src/Syntax/UnifyTy.hs 98
-satisfies t@(ForallT _ c (VarT _)) p =  c `entails` p
+satisfies t@(ForallT c (VarT _)) p =  c `entails` p
hunk ./src/Syntax/UnifyTy.hs 158
-tryInst t (ForallT _ c t') = liftM (\u -> Just (map (\(Pred n t'') -> Pred n (apply u t'')) c)) (match t t')
+tryInst t (ForallT c t') = liftM (\u -> Just (map (\(Pred n t'') -> Pred n (apply u t'')) c)) (match t t')
hunk ./src/Syntax/UnifyTy.hs 160
-tryInst t        t'        = liftM (const (Just [])) (match t t')
+tryInst t       t'       = liftM (const (Just [])) (match t t')
hunk ./src/Syntax/UnifyTy.hs 194
-collectPreds vnm is (ForallT _ c (VarT _)) = liftM concat $ mapM (\p -> bySuper $ mkPred (predClass p) vnm) c
+collectPreds vnm is (ForallT c (VarT _)) = liftM concat $ mapM (\p -> bySuper $ mkPred (predClass p) vnm) c
hunk ./src/Tests.hs 52
-        genforall = do n <- QC.suchThat QC.arbitrary (`S.notMember` visible)
-                       t <- genType (S.insert n visible) kind (pred size)
-                       return $ ForallT [n] [] t
-        consforall = if size > 0 then (genforall:) else id
hunk ./src/Tests.hs 57
-        gens      = conssimple . consforall $ consapp []
+        gens      = conssimple $ consapp []
hunk ./src/Tests.hs 59
-kindOf (VarT {})       = Star
-kindOf (AppT t _)      = let _ `Arrow` r = kindOf t in r
-kindOf (ForallT _ _ t) = kindOf t
-kindOf c@(ConT {})     = fromJust $ lookup c simpleTypeKinds
+kindOf (VarT {})     = Star
+kindOf (AppT t _)    = let _ `Arrow` r = kindOf t in r
+kindOf (ForallT _ t) = kindOf t
+kindOf c@(ConT {})   = fromJust $ lookup c simpleTypeKinds
hunk ./src/Tests.hs 67
-  shrink a@(AppT b c)    =
+  shrink a@(AppT b c)  =
hunk ./src/Tests.hs 70
-  shrink (ForallT _ _ t) = [t]
-  shrink (VarT n)        = map VarT (QC.shrink n)
-  shrink (ConT n)        = []
+  shrink (ForallT _ t) = [t]
+  shrink (VarT n)      = map VarT (QC.shrink n)
+  shrink (ConT n)      = []