Removed imports of TypeCheck.Concrete, fixed problems in TypeCheck.RConcrete

+ The current type checker for concrete syntax is in
  GF.Compile.TypeCheck.RConcrete, but GF.Compile.TypeCheck.Concrete was
  still imported in GFI.

+ Fixed a bug that allowed Ints n as a subtype of Ints m, regardless of
  m and n. It now requires n<=m. Note: the type checker still allows Int
  as a subtype of Ints m, regardless of m.

+ Fixed a potential efficiency problem with large record types, by reducing
  the number of recursive calls from |R|*|S| to |R| when checking if R<=S.

+ Fixed a misleading comment: "alpha g t u" checks that u is a subtype of t,
  the other way around. Similarly, "checkIfEqLType gr g t u trm" checks that
  u is a subtype of t, not the other way around, and not that t is equal to u.

src/compiler/GF/Compile/TypeCheck/Concrete.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE PatternGuards #-}
-module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
-
+module GF.Compile.TypeCheck.Concrete( {-checkLType, inferLType, computeLType, ppType-} ) where
+{-
 import GF.Infra.CheckM
 import GF.Data.Operations
 
@@ -714,3 +714,4 @@ checkLookup x g =
   case [ty | (b,y,ty) <- g, x == y] of
     []     -> checkError (text "unknown variable" <+> ppIdent x)
     (ty:_) -> return ty
+-}

src/compiler/GF/Compile/TypeCheck/RConcrete.hs

@@ -650,7 +650,7 @@ checkIfEqLType gr g t u trm = do
 
   where
 
-   -- t is a subtype of u 
+   -- check that u is a subtype of t
    --- quick hack version of TC.eqVal
    alpha g t u = case (t,u) of  
 
@@ -662,12 +662,13 @@ checkIfEqLType gr g t u trm = do
                               
      -- record subtyping
      (RecType rs, RecType ts) -> all (\ (l,a) -> 
-                                   any (\ (k,b) -> alpha g a b && l == k) ts) rs
+                                   any (\ (k,b) -> l == k && alpha g a b) ts) rs
      (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
      (ExtR r s, t) -> alpha g r t || alpha g s t
 
      -- the following say that Ints n is a subset of Int and of Ints m >= n
-     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> m >= n
+     -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
+     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
            | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
            | t == typeInt,           Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
 

src/compiler/GFI.hs

@@ -17,7 +17,7 @@ import GF.Grammar.Lookup (allOpers,allOpersTo)
 import GF.Compile.Rename(renameSourceTerm)
 --import GF.Compile.Compute.Concrete (computeConcrete,checkPredefError)
 import qualified GF.Compile.Compute.ConcreteNew as CN(normalForm,resourceValues)
-import GF.Compile.TypeCheck.Concrete (inferLType,ppType)
+import GF.Compile.TypeCheck.RConcrete as TC(inferLType,ppType)
 import GF.Infra.Dependencies(depGraph)
 import GF.Infra.CheckM
 import GF.Infra.UseIO(ioErrorText)
@@ -226,7 +226,7 @@ execute1 opts gfenv0 s0 =
           let sigs = [(op,ty) | ((mo,op),ty,pos) <- ops]
           let printer = if isRaw 
                           then showTerm sgr TermPrintDefault Qualified
-                          else (render . GF.Compile.TypeCheck.Concrete.ppType)
+                          else (render . TC.ppType)
           let printed = [unwords [showIdent op, ":", printer ty] | (op,ty) <- sigs]
           mapM_ putStrLn [l | l <- printed, all (flip isInfixOf l) greps]
           continue gfenv