Make user-defined types searchable

[byorgey]

Should be able to handle this similarly to #317.

[byorgey]

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).

[byorgey]

OK, but note to make this work, enumerate also has to handle user-defined types!

[byorgey]

+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

[byorgey]

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.

[byorgey]

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.