fixed what appears to be a bug in how unicode imports worked, and updated the bounds

Author: Matthew Mirman

Diff for: caledon.cabal

@@ -45,10 +45,10 @@ executable caledon
                  containers >= 0.4 && < 1.0, 
                  transformers >= 0.3 && < 1.0,
                  cpphs >= 1.0 && < 2.0,
-                 lens >= 3.0 && < 4.0,
+                 lens >= 3.0,
                  deepseq >= 1 && < 2,
                  spoon >= 0 && < 1,
-                 fgl >= 5.4 && < 5.5
+                 fgl >= 5.4
 
   Extensions: FlexibleContexts,
               FlexibleInstances,

Diff for: sources/HOU.hs

@@ -4,15 +4,18 @@
  UnicodeSyntax,
  BangPatterns,
  TupleSections,
- ViewPatterns
+ ViewPatterns,
+ FlexibleContexts
  #-}
 module HOU where
 
+
 import Src.Tracing
 import Names
 import Choice
 import AST
 import Substitution
+
 import Context
 import TopoSortAxioms
 import Control.Monad.State.Strict (StateT, forM_,runStateT, modify, get,put, State, runState)
@@ -34,6 +37,11 @@ import System.IO.Unsafe
 
 import Control.Lens hiding (Choice(..))
 
+-- No idea why I would need to redefine these here
+(.∀) :: Name -> Type -> Constraint -> Constraint
+(.∀) = Bind Forall
+      
+
 throwTrace !i s = vtrace i s $ throwError s
 
 -----------------------------------------------
@@ -689,7 +697,7 @@ checkType b sp ty = case sp of
     t'' <- regenAbsVars t
     v'  <- checkType b v'' t
     r   <- getNewWith "@r"
-    Spine _ l' <- addToEnv (∀) r t'' $ checkType b (Spine r l) ty
+    Spine _ l' <- addToEnv (.∀) r t'' $ checkType b (Spine r l) ty
     if b 
       then return $ rebuildSpine (rebuildFromMem mem v') l'
       else return $ rebuildSpine (ascribe (rebuildFromMem mem v') t) l'
@@ -706,20 +714,20 @@ checkType b sp ty = case sp of
 
   Spine "#imp_forall#" [_, Abs x tyA tyB] -> do
     tyA <- checkType b tyA tipe
-    tyB <- addToEnv (∀) x tyA $ checkType b tyB ty
+    tyB <- addToEnv (.∀) x tyA $ checkType b tyB ty
     return $ imp_forall x tyA tyB
 
   Spine "#forall#" [_, Abs x tyA tyB] -> do
     tyA <- checkType b tyA tipe
-    forall x tyA <$> (addToEnv (∀) x tyA $ 
+    forall x tyA <$> (addToEnv (.∀) x tyA $ 
       checkType b tyB ty )
 
   -- below are the only cases where bidirectional type checking is useful 
   Spine "#imp_abs#" [_, Abs x tyA sp] -> case ty of
     Spine "#imp_forall#" [_, Abs x' tyA' tyF'] | x == x' || "" == x' -> do
       tyA <- checkType b tyA tipe
       tyA ≐ tyA'
-      addToEnv (∀) x tyA $ do
+      addToEnv (.∀) x tyA $ do
         imp_abs x tyA <$> checkType b sp tyF'
     _ -> do
       -- here this acts like "infers" since we can always initialize a ?\ like an infers!
@@ -733,14 +741,14 @@ checkType b sp ty = case sp of
     Spine "#forall#" [_, Abs x' tyA' tyF'] -> do
       tyA <- checkType b tyA tipe
       tyA ≐ tyA'
-      addToEnv (∀) x tyA $ do
+      addToEnv (.∀) x tyA $ do
         Abs x tyA <$> checkType b sp (subst (x' |-> var x) tyF')
     _ -> do
       e <- getNewWith "@e"
       tyA <- checkType b tyA tipe
       addToEnv (∃) e (forall "" tyA tipe) $ do
         forall x tyA (Spine e [var x]) ≐ ty
-        Abs x tyA <$> addToEnv (∀) x tyA (checkType b sp $ Spine e [var x])
+        Abs x tyA <$> addToEnv (.∀) x tyA (checkType b sp $ Spine e [var x])
   Spine nm [] | isChar nm -> do
     ty ≐ Spine "char" []
     return sp

Diff for: sources/Main.hs

@@ -3,10 +3,10 @@ module Main where
 
 import Options
 import AST
+import HOU
 import Substitution
 import Src.Tracing
 import Choice
-import HOU
 import qualified Src.Pipeline as Src
 import Parser
 import System.Environment
@@ -101,4 +101,4 @@ main = do
   processFile $ options & case files of
     [] -> id
     [fname] -> optFile .~ fname
-    _ -> error $ "Too many file arguments."++header
+    _ -> error $ "Too many file arguments."++header

Diff for: sources/Parser.hs

@@ -29,7 +29,7 @@ import qualified Data.Set as S
 import Debug.Trace
 import qualified Data.Foldable as F
 
-import Control.Lens 
+import Control.Lens hiding (noneOf)
 
 -----------------------------------------------------------------------
 -------------------------- PARSER -------------------------------------

Diff for: sources/Src/Elaborate.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE  
- ViewPatterns
+ ViewPatterns,
+ FlexibleContexts
  #-}
 module Src.Elaborate (typeConstraints) where
 
@@ -155,4 +156,4 @@ getType (a :+: v) = do
     Just ~(ty,t') -> do
       return $ fromType $ appN' (Abs ty $ Pat t') v
 
-    
+    

Diff for: sources/Substitution.hs

@@ -233,7 +233,10 @@ instance Subst Constraint where
 
 subq s f e c1 c2 = e (substFree s f c1) (substFree s f c2)
 
+(∃) :: Name -> Type -> Constraint -> Constraint
 (∃) = Bind Exists
+
+(∀) :: Name -> Type -> Constraint -> Constraint
 (∀) = Bind Forall
 
 infixr 0 <<$>
@@ -346,4 +349,4 @@ eta_expandAll mp (Spine s l) = case mp ! s of
   Nothing -> Spine s (eta_expandAll mp <$> l)
   Just t  -> rebuildSpine (eta_expand t s) (eta_expandAll mp <$> l)
 
-  
+