Correctly chain coercions for type functions

This adds transitivity coercions to core and syntax. And a whole lot of
stuff which I made @zardyh do. Sorry. 🖤

Closes #202

src/Core/Core.hs

@@ -144,6 +144,7 @@ data Capture a = Capture a (Type a)
 data Coercion a
  = SameRepr (Type a) (Type a)
  | Symmetry (Coercion a)
+ | Trans (Coercion a) (Coercion a)
 
  | Application (Coercion a) (Coercion a)
  | Quantified (BoundTv a) (Coercion a) (Coercion a)
@@ -224,13 +225,14 @@ instance (Annotation b, Pretty a) => Pretty (AnnTerm b a) where
 
 instance Pretty a => Pretty (Coercion a) where
  pretty (SameRepr a b) = pretty a <+> soperator (char '~') <+> pretty b
- pretty (Application c c') = pretty c <+> pretty c'
+ pretty (Application c c') = pretty c <+> parens (pretty c')
  pretty (Record r s) = enclose (lbrace <> space) (space <> rbrace) (pretty r <+> hsep (punctuate comma (map pprCoRow s)))
  pretty (ExactRecord r) = enclose (lbrace <> space) (space <> rbrace) (hsep (punctuate comma (map pprCoRow r)))
  pretty (Projection _ rs') =
  enclose (lbrace <> space) (space <> rbrace)
  (keyword "proj" <+> hsep (punctuate comma (map pprCoRow rs')))
  pretty (Symmetry f) = keyword "sym" <+> parens (pretty f)
+ pretty (Trans x y) = parens (pretty x) <+> soperator (char '∘') <+> parens (pretty y)
  pretty (Quantified (Relevant v) dom c) = keyword "∀" <> (pretty v <+> colon <+> pretty dom) <> dot <+> pretty c
  pretty (Quantified Irrelevant dom c) = pretty dom <+> arrow <+> pretty c
  pretty (CoercionVar x) = pretty x
@@ -418,6 +420,10 @@ relates (Projection rs rs') = do
 relates (Symmetry x) = do
  (a, b) <- relates x
  pure (b, a)
+relates (Trans x y) = do
+ (a, _) <- relates x
+ (_, b) <- relates y
+ pure (a, b)
 relates (Quantified v co c) = do
  (a, b) <- relates c
  (c, d) <- relates co

src/Core/Lint.hs

@@ -16,6 +16,7 @@ import qualified Data.VarMap as VarMap
 import qualified Data.VarSet as VarSet
 import qualified Data.Sequence as Seq
 import qualified Data.Text as T
+import Data.Functor.Constant
 import Data.Traversable
 import Data.Foldable
 import Data.Function
@@ -206,7 +207,7 @@ checkTerm s (Lam arg@(TypeArgument a ty) bod) = do
  errs <- gatherError' . liftError $
  -- Ensure type is valid and we're declaring a tyvar
  unless (varInfo a == TypeVar) (pushError (InfoIllegal a TypeVar (varInfo a)))
- *> checkType s ty
+ *> checkType (s { tyVars = VarSet.insert (toVar a) (tyVars s) }) ty
 
  (bty, bod') <- checkTerm (s { tyVars = VarSet.insert (toVar a) (tyVars s) }) bod
  pure ( ForallTy (Relevant a) ty <$> bty
@@ -343,8 +344,9 @@ checkTypeBoxed s x = checkType s x *> checkNoUnboxed x
 --
 -- Ideally this would use ApplicativeDo, but GHC is still a little silly at
 -- desugaring it all.
-checkCoercion :: IsVar a => Scope a -> Coercion a -> Errors (CoreErrors a) (Type a, Type a)
+checkCoercion :: forall a. IsVar a => Scope a -> Coercion a -> Errors (CoreErrors a) (Type a, Type a)
 checkCoercion s = checkCo where
+ checkCo :: Coercion a -> Errors (CoreErrors a) (Type a, Type a)
  checkCo (SameRepr a b) =
  checkType s a
  *> checkType s b
@@ -383,6 +385,12 @@ checkCoercion s = checkCo where
  _ -> pushError (InvalidCoercion (Axiom ax i))
 
  checkCo (Symmetry x) = swap <$> checkCo x
+ checkCo co@(Trans x y) =
+ (\((tx, ty), (ty', tz)) ->
+ (if ty `apart` ty'
+ then failure (Seq.fromList [ InvalidCoercion co, TypeMismatch ty ty' ])
+ else pure ())
+ $> (tx, tz)) `bindErrors` ((,) <$> checkCo x <*> checkCo y)
  checkCo (Quantified v l r) =
  (\(f, g) (x, y) -> (ForallTy v f x, ForallTy v g y)) <$> checkCo l <*> checkCo r
 
@@ -392,11 +400,15 @@ checkCoercion s = checkCo where
  coAxT x = error (show x)
 
  checkCoAx _ (coAxT -> ts) args =
- (VarTy (fromVar tyvarA), snd (last ts))
- -- TODO: This is quite sad. Can we fix it? See lint/tyfun-unsat.ml
- <$ traverse_ checkCo' (zip ts args)
- checkCo' ((a, b), co) = (\(l, r) -> if (a `apart` l) || (b `apart` r) then pushError (InvalidCoercion co) else pure ())
- <$> checkCo co
+ (\sub -> bimap (substituteInType sub) (substituteInType sub) (last ts)) . fold
+ <$> traverse checkCo' (zip ts args)
+
+ checkCo' ((a, b), co) =
+ (\(l, r) ->
+ case (unify a l, unify b r) of
+ (Just a, Just b) -> pure ((a <> b) `VarMap.withoutKeys` VarSet.toList (tyVars s))
+ (_, _) -> pushError (InvalidCoercion co))
+ `bindErrors` checkCo co
 
 checkPattern :: forall a. IsVar a => Scope a -> Type a -> Pattern a -> Errors (CoreErrors a) ()
 checkPattern s = checkPat where
@@ -524,3 +536,7 @@ patternVars PatWildcard{} = []
 
 captureVars :: Capture a -> (a, Type a)
 captureVars (Capture v ty) = (v, ty)
+
+bindErrors :: (a -> Errors e b) -> Errors e a -> Errors e b
+bindErrors f (Pure a) = f a
+bindErrors _ (Other (Constant x)) = failure x

src/Core/Lower.hs

@@ -204,6 +204,7 @@ co (S.VarCo x) = CoercionVar (mkCo x)
 co (S.ReflCo t) = SameRepr (lowerType t) (lowerType t)
 co (S.AssumedCo t t') = SameRepr (lowerType t) (lowerType t')
 co (S.SymCo c) = Symmetry (co c)
+co (S.TransCo x y) = Trans (co x) (co y)
 co (S.AppCo a b) = Application (co a) (co b)
 co (S.ArrCo a b) = C.Quantified Irrelevant (co a) (co b)
 co (S.ProdCo a b) = ExactRecord [("_1", co a), ("_2", co b)]

src/Core/Optimise.hs

@@ -65,6 +65,7 @@ substituteInTys = term where
 
  coercion m (SameRepr t t') = SameRepr (gotype m t) (gotype m t')
  coercion m (Symmetry c) = Symmetry (coercion m c)
+ coercion m (Trans x y) = Trans (coercion m x) (coercion m y)
  coercion m (Application f x) = Application (coercion m f) (coercion m x)
  coercion m (ExactRecord rs) = ExactRecord (map (second (coercion m)) rs)
  coercion m (Record c rs) = Record (coercion m c) (map (second (coercion m)) rs)
@@ -120,6 +121,7 @@ substituteInCo m c
 
  coercion (SameRepr t t') = SameRepr (gotype t) (gotype t')
  coercion (Symmetry c) = Symmetry (coercion c)
+ coercion (Trans x y) = Trans (coercion x) (coercion y)
  coercion (Application f x) = Application (coercion f) (coercion x)
  coercion (ExactRecord rs) = ExactRecord (map (second coercion) rs)
  coercion (Record c rs) = Record (coercion c) (map (second coercion) rs)

src/Data/VarMap.hs

@@ -5,6 +5,7 @@ module Data.VarMap
  , lookup, member, findWithDefault
  , insert, delete
  , map, mapWithKey, singleton, union, unionSemigroup
+ , withoutKeys
  , alter
  , difference, intersection
  , foldrWithKey, foldr
@@ -14,6 +15,7 @@ module Data.VarMap
 import Control.Lens (At(..), Ixed(..), Index, IxValue)
 import qualified Data.HashMap.Strict as Map
 import qualified Prelude as P
+import Data.Foldable (foldl')
 import Data.Coerce
 import Prelude hiding (lookup, map, null, foldr)
 
@@ -69,7 +71,7 @@ alter f k (Map m) = Map (Map.alter f k m)
 mapWithKey :: (CoVar -> a -> b) -> Map a -> Map b
 mapWithKey f (Map a) = Map (Map.mapWithKey f a)
 
-singleton :: CoVar -> a ->  Map a
+singleton :: CoVar -> a -> Map a
 singleton x v = coerce (Map.singleton x v)
 
 unionSemigroup :: Semigroup a => Map a -> Map a -> Map a
@@ -78,6 +80,9 @@ unionSemigroup (Map l) (Map r) = Map (Map.unionWith (<>) l r)
 foldrWithKey :: (CoVar -> a -> b -> b) -> b -> Map a -> b
 foldrWithKey f b (Map m) = Map.foldrWithKey f b m
 
+withoutKeys :: Map a -> [CoVar] -> Map a
+withoutKeys (Map a) keys = Map (foldl' (flip Map.delete) a keys)
+
 foldr :: (a -> b -> b) -> b -> Map a -> b
 foldr f b (Map m) = Map.foldr f b m
 

src/Syntax/Subst.hs

@@ -70,6 +70,7 @@ instance Ord (Var p) => Substitutable p (Coercion p) where
  ftv (ReflCo t) = ftv t
  ftv (AssumedCo t t') = ftv t <> ftv t'
  ftv (SymCo c) = ftv c
+ ftv (TransCo x y) = ftv x <> ftv y
  ftv (AppCo f x) = ftv f <> ftv x
  ftv (ArrCo f x) = ftv f <> ftv x
  ftv (ProdCo f x) = ftv f <> ftv x
@@ -90,6 +91,7 @@ instance Ord (Var p) => Substitutable p (Coercion p) where
  apply s (ReflCo t) = ReflCo (apply s t)
  apply s (AssumedCo t t') = AssumedCo (apply s t) (apply s t')
  apply s (SymCo x) = SymCo (apply s x)
+ apply s (TransCo x y) = TransCo (apply s x) (apply s y)
  apply s (AppCo f x) = AppCo (apply s f) (apply s x)
  apply s (ArrCo f x) = ArrCo (apply s f) (apply s x)
  apply s (ProdCo f x) = ProdCo (apply s f) (apply s x)

src/Syntax/Transform.hs

@@ -52,6 +52,7 @@ transformCoercion fc ft = goC where
  transC (P2 c) = P2 c
  transC (MvCo c) = P2 c
  transC (ReflCo l) = ReflCo (goT l)
+ transC (TransCo x y) = TransCo (goC x) (goC y)
  transC (AssumedCo l r) = AssumedCo (goT l) (goT r)
  transC (AppCo f x) = AppCo (goC f) (goC x)
  transC (ArrCo f x) = ArrCo (goC f) (goC x)

src/Syntax/Type.hs

@@ -100,6 +100,7 @@ data Coercion p
  | MvCo (Var p) -- coercion metavariable
  | ReflCo (Type p) -- <T> : T ~ T
  | SymCo (Coercion p) -- sym (X : T ~ S) : S ~ T
+ | TransCo (Coercion p) (Coercion p) -- trans (X : T ~ S) (Y : S ~ U) : T ~ U
  | AppCo (Coercion p) (Coercion p) -- (f : B ~ D) (x : A ~ C) : B A ~ D C
  | ArrCo (Coercion p) (Coercion p) -- (x : S ~ T) -> (y : S' ~ T') : (S -> S') ~ (T -> T')
  | ProdCo (Coercion p) (Coercion p) -- (x : S ~ T, y : S' ~ T') : (S, S') ~ (T, T')
@@ -153,6 +154,7 @@ instance Pretty (Var p) => Pretty (Coercion p) where
  pretty (ReflCo t) = enclose (char '<') (char '>') (pretty t)
  pretty (AssumedCo a b) = enclose (char '<') (char '>') (pretty a <> comma <+> pretty b)
  pretty (SymCo x) = keyword "sym" <+> pretty x
+ pretty (TransCo x y) = parens (pretty x) <+> soperator (char '∘') <+> parens (pretty y)
  pretty (AppCo f x) = pretty f <+> pretty x
  pretty (ArrCo f x) = pretty f <+> arrow <+> pretty x
  pretty (ProdCo f x) = pretty f <+> prod <+> pretty x

src/Types/Infer/Builtin.hs

@@ -69,7 +69,11 @@ leakEqualities :: ( Reasonable f p
  => f p
  -> [(Type Typed, Type Typed)]
  -> m ()
-leakEqualities r ((a, b):xs) = unify (BecauseOf r) a b *> leakEqualities r xs
+leakEqualities r ((a, b):xs) = do
+ x <- genName
+ i <- view classes
+ tell (Seq.singleton (ConImplicit (BecauseOf r) i x (TyApps tyEq [a, b])))
+ leakEqualities r xs
 leakEqualities _ [] = pure ()
 
 decompose :: MonadInfer Typed m

src/Types/Infer/Class.hs

@@ -414,7 +414,7 @@ inferInstance inst@(Instance clss ctx instHead bindings ann) = do
  axiom_t = close $
  foldr (TyPi . Anon)
  (TyApps tyEq [ TyApps (TyCon var) (instArgs ++ map TyVar argvs), exp])
- ( zipWith (\a b -> TyApps tyEq [a, b]) classArgs instArgs
+ ( zipWith (\a b -> TyApps tyEq [b, a]) classArgs instArgs
  ++ map (\a -> TyApps tyEq [TyVar a, TyVar a]) argvs)
  close t = foldr (\v -> TyPi (Invisible v (Just TyType) Req)) t (ftv t)
  pure (info, axdef)

src/Types/Infer/Function.hs

@@ -113,7 +113,7 @@ makeTypeFunctionHIT args = traverse go where
  name <- genName
  let (TyApps tyfun args') = lhs
  argtvs = map (\(TyAnnArg a _) -> a) args
- needs = zipWith (\a b -> TyApps tyEq [TyVar a, b]) argtvs args'
+ needs = zipWith (\a b -> TyApps tyEq [b, TyVar a]) argtvs args'
  tau = foldr TyArr (TyApps tyEq [TyApps tyfun (map TyVar argtvs), rhs]) needs
  fv = Set.toList (ftv tau)
  closed = foldr (\v -> TyPi (Invisible v (Just TyType) Spec)) tau fv

src/Types/Unify.hs

@@ -807,8 +807,8 @@ tyFunByEval (TyFamInfo tn eqs relevant _ con) scope args tb = do
  then do
  let r_t = foldl TyApp (apply sub result) (apply sub rest_args)
  traceM (displayS (keyword "[D]:" <+> pretty r_t <+> "~" <+> pretty tb))
- _ <- unify scope r_t tb
- pure (Just (foldl AppCo (InstCo con cos) (map ReflCo rest_args)))
+ other_co <- unify scope r_t tb
+ pure (pure (foldl AppCo (InstCo con cos) (map ReflCo rest_args) `TransCo` other_co))
 
  else pure Nothing
 

tests/driver/Test/Types/Unify.hs

@@ -49,6 +49,10 @@ provenCoercion P2{} = undefined
 provenCoercion InstCo{} = undefined
 provenCoercion (SymCo c)
  | (a, b) <- provenCoercion c = (b, a)
+provenCoercion (TransCo x y)
+ | (a, _) <- provenCoercion x
+ , (_, c) <- provenCoercion y
+ = (a, c)
 provenCoercion (AppCo c c')
  | (f, f') <- provenCoercion c, (x, x') <- provenCoercion c'
  = (TyApp f x, TyApp f' x')

tests/lint/tyfun-unsat.ml

@@ -2,6 +2,6 @@ type function get_con 'a begin
  get_con ('f 'a) = 'f
 end
 
-type 'a ~~ 'b = Refl : 'a ~~ 'a
+type 'a ~~ 'b = Refl : 'a ~~ 'b
 
 let _ : (get_con (list int) ~~ list) = Refl

tests/types/class/fundep02.out

@@ -10,8 +10,8 @@ AddS : Infer{'il : type}. Infer{'im : type}. Spec{'a : 'il}. Spec{'c : 'im}. Spe
 add : nat -> nat -> nat -> constraint
 ev : Spec{'a : nat}. Spec{'b : nat}. Spec{'c : nat}. add 'a 'b 'c => add_ev 'a 'b 'c
 vect : nat -> type -> type
-Nil : Infer{'wj : type}. Spec{'n : 'wj}. Spec{'a : type}. ('n ~ Z) ⊃ vect 'n 'a
-Cons : Infer{'xr : type}. Spec{'n : 'xr}. Spec{'a : type}. Spec{'n : nat}. ('n ~ S 'n) ⊃ ('a * vect 'n 'a) -> vect 'n 'a
+Nil : Infer{'wy : type}. Spec{'n : 'wy}. Spec{'a : type}. ('n ~ Z) ⊃ vect 'n 'a
+Cons : Infer{'yg : type}. Spec{'n : 'yg}. Spec{'a : type}. Spec{'n : nat}. ('n ~ S 'n) ⊃ ('a * vect 'n 'a) -> vect 'n 'a
 append_with : Spec{'k : nat}. Spec{'l : nat}. Spec{'n : nat}. Spec{'a : type}. add_ev 'n 'k 'l -> vect 'n 'a -> vect 'k 'a -> vect 'l 'a
 append : Infer{'k : nat}. Infer{'l : nat}. Infer{'n : nat}. Infer{'a : type}. add 'n 'k 'l => vect 'n 'a -> vect 'k 'a -> vect 'l 'a
 :: : Infer{'a : type}. Infer{'n : nat}. 'a -> vect 'n 'a -> vect (S 'n) 'a

tests/types/gadt/fail_term.out

@@ -1,4 +1,9 @@
 fail_term.ml[16:3 ..16:30]: error
+ No instance for 'a -> 'b -> 'b ~ 'b -> 'y -> 'b arising in this expression
+ │ 
+16 │ Lam (Lam (Var (There Here)))
+ │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ • Because:
  Could not match the rigid type variable 'b with the type 'a
 
  • Arising in this expression

tests/types/gadt/fin.out

@@ -1,6 +1,11 @@
 fin.ml[11:14 ..11:18]: error
+ No instance for 'n ~ S (S 'k) arising in this expression
  │ 
 11 │ | SS SZ -> FS FZ
  │ ^^^^^
- Couldn't match actual type fin (S (S 'k))
- with the type expected by the context, fin 'n
+ • Because:
+ │ 
+11 │ | SS SZ -> FS FZ
+ │ ^^^^^
+ Couldn't match actual type 'n ~ 'n
+ with the type expected by the context, 'n ~ S (S 'k)

tests/types/gadt/gadt03-fail.out

@@ -1,6 +1,11 @@
 gadt03-fail.ml[8:12 ..8:19]: error
+ No instance for bool ~ int arising in the expression
  │ 
 8 │ let show = function
  │ ^^^^^^^^
- Couldn't match actual type int
- with the type expected by the context, bool
+ • Because:
+ │ 
+8 │ let show = function
+ │ ^^^^^^^^
+ Couldn't match actual type bool ~ bool
+ with the type expected by the context, bool ~ int

tests/types/gadt/gadt07-escape-fail.out

@@ -1,4 +1,9 @@
 gadt07-escape-fail.ml[10:3 ..10:17]: error
+ No instance for 'a ~ int arising in the expression
+ │ 
+10 │ match hval with
+ │ ^^^^^^^^^^^^^^^
+ • Because:
  Could not match the rigid type variable 'a with the type int
 
  Where the type variable a is an existential,

tests/types/gadt/pass_term.out

@@ -8,4 +8,4 @@ term : type -> type -> type
 Var : Spec{'ctx : type}. Spec{'ty : type}. elem 'ty 'ctx -> term 'ctx 'ty
 Lam : Infer{'mu : type}. Spec{'ty : 'mu}. Spec{'a : type}. Spec{'b : type}. Spec{'ctx : type}. ('ty ~ 'a -> 'b) ⊃ term ('a * 'ctx) 'b -> term 'ctx 'ty
 App : Infer{'ov : type}. Spec{'ty : 'ov}. Spec{'a : type}. Spec{'b : type}. Spec{'ctx : type}. ('ty ~ 'b) ⊃ (term 'ctx ('a -> 'b) * term 'ctx 'a) -> term 'ctx 'ty
-const : Infer{'a : type}. Infer{'ctx : type}. Infer{'b : type}. term 'ctx ('a -> 'b -> 'a)
+const : Infer{'b : type}. Infer{'y : type}. Infer{'xs : type}. term 'xs ('b -> 'y -> 'b)

tests/types/nasty_cycle.out

@@ -1,4 +1,4 @@
-nasty_cycle.ml[18:19 ..18:33]: error
+nasty_cycle.ml[19:20 ..19:25]: error
  Could not match the rigid type variable 's with the type S 's
 
  Where the type variable s is an existential,
@@ -7,9 +7,14 @@ nasty_cycle.ml[18:19 ..18:33]: error
 
  • Arising in the this expression
  │ 
+19 │ | Right p -> Left p
+ │ ^^^^^^
+nasty_cycle.ml[18:26 ..18:32]: error
+ No instance for S 'n ~ S (S 's) arising in this expression
+ │ 
 18 │ | Left p -> Right (Even2 p)
- │ ^^^^^^^^^^^^^^^
-nasty_cycle.ml[19:20 ..19:25]: error
+ │  ^^^^^^^
+ • Because:
  Could not match the rigid type variable 's with the type S 's
 
  Where the type variable s is an existential,
@@ -18,5 +23,5 @@ nasty_cycle.ml[19:20 ..19:25]: error
 
  • Arising in the this expression
  │ 
-19 │ | Right p -> Left p
- │ ^^^^^^
+18 │ | Left p -> Right (Even2 p)
+ │  ^^^^^^^

tests/types/tyfun/chain.ml

@@ -0,0 +1,9 @@
+type function bar 'a begin
+ bar int = int
+end
+
+type function foo 'a begin
+ foo 'a = bar 'a
+end
+
+let x : foo int = 123

tests/types/tyfun/chain.out

@@ -0,0 +1,3 @@
+bar : type -> type
+foo : type -> type
+x : foo int

tests/types/tyfun/tyfun02-fail.out

@@ -2,4 +2,4 @@ tyfun02-fail.ml[11:16 ..12:10]: error
  │ 
 14 │ | _ -> Xs
  │ ^^
- No instance for collapse 'a ~ string arising from this expression
+ No instance for collapse 'a ~ string arising from the expression