Claudio/cyclic bounds #586
Conversation
|
ping @rossberg |
src/as_frontend/typing.ml
Outdated
| @@ -251,8 +251,29 @@ and check_typ_tag env typ_tag = | |||
| let t = check_typ env typ in | |||
| T.{lab = tag.it; typ = t} | |||
|
|
|||
| and check_typ_binds_acyclic env typ_bind cs ts = | |||
There was a problem hiding this comment.
| and check_typ_binds_acyclic env typ_bind cs ts = | |
| and check_typ_binds_acyclic env typ_binds cs ts = |
| let n = List.length cs in | ||
| let ce = List.fold_left2 | ||
| (fun ce c t -> T.ConEnv.add c t ce) T.ConEnv.empty cs ts in | ||
| let chase typ_bind c = |
There was a problem hiding this comment.
This really only needs typ_bind.at
There was a problem hiding this comment.
(Scrap that, forgot to delete.)
src/as_frontend/typing.ml
Outdated
| let chase typ_bind c = | ||
| let rec chase i ts c' = | ||
| if i > n | ||
| then |
There was a problem hiding this comment.
Nit: put on previous line
src/as_frontend/typing.ml
Outdated
| and check_typ_binds_acyclic env typ_bind cs ts = | ||
| let n = List.length cs in | ||
| let ce = List.fold_left2 | ||
| (fun ce c t -> T.ConEnv.add c t ce) T.ConEnv.empty cs ts in |
There was a problem hiding this comment.
You can avoid the extra lambda by using fold_right2.
| (match t with | ||
| | T.Con (c'', []) -> | ||
| chase (i+1) (t::ts) c'' | ||
| | _ -> ()) |
There was a problem hiding this comment.
Is this sufficient? I suspect that without beta reducing outside constructor applications it will not detect, e.g.,
type Id<T> = T;
func f<A <: Id<A>>() = {}
There was a problem hiding this comment.
Dooh. This is the check we had on the CLR but that doesn't have type functions. I'll add a reduction step and tests.
Dunno, that's an interesting question, something like, given k constructors, if you can unfold thos constructors down a path more than k times you've got a cyle - is that enough? In any case, Andrew K seems to think the restriction described by him and Benjamin should be applicable to uniformity. Still on my (our) stack. |
## Changelog for motoko-base: Branch: next-moc Commits: [dfinity/motoko-base@591f5af2...5bbf04cf](dfinity/motoko-base@591f5af...5bbf04c) * [`085468f7`](dfinity/motoko-base@085468f) Apply NaN canonicalization in base tests ([dfinity/motoko-base#586](https://togithub.com/dfinity/motoko-base/issues/586))
## Changelog for motoko-base: Branch: next-moc Commits: [dfinity/motoko-base@591f5af2...5bbf04cf](dfinity/motoko-base@591f5af...5bbf04c) * [`085468f7`](dfinity/motoko-base@085468f) Apply NaN canonicalization in base tests ([dfinity/motoko-base#586](https://togithub.com/dfinity/motoko-base/issues/586))
Reject cyclic bounds.
Instead of doing a top sort, we simply check that, given n type parameters, we can't construct a type parameter chasing subtype derivation of depth >= n.
We do the check both in typing.ml and check_ir.ml.