Open byorgey opened 2 years ago
type T(a) = Unit + a * T(a) * T(a)
!!! forall t : T(N). mirror(mirror(t)) == t
mirror : T(a) -> T(a)
mirror(left(unit)) = left(unit)
mirror(right(a,l,r)) = right(a, mirror(r), mirror(l))
yields
Error: the type
Unit + ℕ × T(ℕ) × T(ℕ)
is not searchable (i.e. it cannot be used in a forall).
OK, but note to make this work, enumerate
also has to handle user-defined types!
+isSearchable :: TyDefCtx -> Type -> Bool
+isSearchable tyDefs = go S.empty
+ where
+ go :: Set (String, [Type]) -> Type -> Bool
+ go _ TyProp = False
+ go _ ty
+ | isNumTy ty = True
+ | isFiniteTy ty = True
+ go seen (TyUser t tys)
+ | (t,tys) `S.member` seen = True
+ | otherwise = case M.lookup t tyDefs of
+ Nothing -> error $ t ++ " not in tydefs!"
+ Just (TyDefBody _ body) -> go (S.insert (t,tys) seen) (body tys)
+ go seen (TyList ty) = go seen ty
+ go seen (TySet ty) = go seen ty
+ go seen (ty1 :+: ty2) = go seen ty1 && go seen ty2
+ go seen (ty1 :*: ty2) = go seen ty1 && go seen ty2
+ go seen (ty1 :->: ty2) = isFiniteTy ty1 && go seen ty2
Above is the code for isSearchable
. Putting this off for now because getting enumerate
to handle user-defined types is a bit tricky. First of all, we have to be able to call enumerate
at runtime, when we no longer have access to the TyDefCtx
(we could, somehow, but it would require some new plumbing). Alternatively, we could translate the encoding of types passed at runtime to use fixpoints, so that we could do without the TyDefCtx
. Then we have to contrive to insert the infinite
enumeration combinator somehow when dealing with an infinite user-defined type, or else it will just hang.
Using fixpoints sounds nice and tidy, but it would require some work when parsing type definitions: we would have to do some analysis to figure out mutually recursive groups of type definitions and then somehow translate each group into a single fixpoint.
Should be able to handle this similarly to #317.