Make join on types always reflexive.

jackohughes · Mar 13, 2019 · b114214 · b114214
1 parent 1688cf4
commit b114214
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/frontend/src/Language/Granule/Checker/Types.hs b/frontend/src/Language/Granule/Checker/Types.hs
@@ -394,6 +394,8 @@ isDualSession sp _ t1 t2 _ = throw
 
 -- Essentially equality on types but join on any coeffects
 joinTypes :: (?globals :: Globals) => Span -> Type -> Type -> Checker Type
+joinTypes s t t' | t == t' = return t
+
 joinTypes s (FunTy t1 t2) (FunTy t1' t2') = do
   t1j <- joinTypes s t1' t1 -- contravariance
   t2j <- joinTypes s t2 t2'
@@ -452,4 +454,4 @@ joinTypes s (TyVar _) t = return t
 joinTypes s t (TyVar _) = return t
 
 joinTypes s t1 t2 = throw
-  NoUpperBoundError{ errLoc = s, errTy1 = t1, errTy2 = t2 }
+  NoUpperBoundError{ errLoc = s, errTy1 = t1, errTy2 = t2 }