diff --git a/frontend/src/Language/Granule/Checker/Types.hs b/frontend/src/Language/Granule/Checker/Types.hs index 549f58c24..3ebd153ea 100644 --- 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 } \ No newline at end of file + NoUpperBoundError{ errLoc = s, errTy1 = t1, errTy2 = t2 }