Throw an error instead of crashing on impredicative types

src/Swarm/Language/Pretty.hs

@@ -300,6 +300,8 @@ instance PrettyPrec TypeErr where
     "Record does not have a field with name" <+> pretty x <> ":" <+> ppr t
   prettyPrec _ (InvalidAtomic reason t) =
     "Invalid atomic block:" <+> ppr reason <> ":" <+> ppr t
+  prettyPrec _ Impredicative =
+    "Unconstrained unification type variables encountered, likely due to an impredicative type. This is a known bug; for more information see https://github.com/swarm-game/swarm/issues/351 ."
 
 -- | Given a type and its source, construct an appropriate description
 --   of it to go in a type mismatch error message.

src/Swarm/Language/Typecheck.hs

@@ -57,7 +57,7 @@ import Control.Arrow ((***))
 import Control.Category ((>>>))
 import Control.Lens ((^.))
 import Control.Lens.Indexed (itraverse)
-import Control.Monad (forM_, void, when)
+import Control.Monad (forM_, void, when, (<=<))
 import Control.Monad.Except (
   ExceptT,
   MonadError (catchError, throwError),
@@ -182,15 +182,18 @@ runTC ctx =
     >>> ( >>=
             \(Module u uctx) ->
               Module
-                <$> mapM (fmap fromU . generalize) u
-                <*> pure (fromU uctx)
+                <$> mapM (checkPredicative <=< (fmap fromU . generalize)) u
+                <*> checkPredicative (fromU uctx)
         )
     >>> flip runReaderT (toU ctx)
     >>> flip runReaderT []
     >>> runExceptT
     >>> evalIntBindingT
     >>> runIdentity
 
+checkPredicative :: Maybe a -> TC a
+checkPredicative = maybe (throwError (mkRawTypeErr Impredicative)) pure
+
 -- | Look up a variable in the ambient type context, either throwing
 --   an 'UnboundVar' error if it is not found, or opening its
 --   associated 'UPolytype' with fresh unification variables via
@@ -431,6 +434,9 @@ data TypeErr
     UnknownProj Var Term
   | -- | An invalid argument was provided to @atomic@.
     InvalidAtomic InvalidAtomicReason Term
+  | -- | Some unification variables ended up in a type, probably due to
+    --   impredicativity.  See https://github.com/swarm-game/swarm/issues/351 .
+    Impredicative
   deriving (Show)
 
 -- | Various reasons the body of an @atomic@ might be invalid.

src/Swarm/Language/Types.hs

@@ -83,7 +83,6 @@ import Data.Kind qualified
 import Data.Map.Merge.Strict qualified as M
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as M
-import Data.Maybe (fromJust)
 import Data.Set (Set)
 import Data.Set qualified as S
 import Data.String (IsString (..))
@@ -223,7 +222,8 @@ type UCtx = Ctx UPolytype
 -- | A @Poly t@ is a universally quantified @t@.  The variables in the
 --   list are bound inside the @t@.  For example, the type @forall
 --   a. a -> a@ would be represented as @Forall ["a"] (TyFun "a" "a")@.
-data Poly t = Forall [Var] t deriving (Show, Eq, Functor, Data, Generic, FromJSON, ToJSON)
+data Poly t = Forall [Var] t
+  deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, FromJSON, ToJSON)
 
 -- | A polytype without unification variables.
 type Polytype = Poly Type
@@ -259,20 +259,20 @@ class WithU t where
   --   Generally, this direction requires somehow knowing that there
   --   are no longer any unification variables in the value being
   --   converted.
-  fromU :: U t -> t
+  fromU :: U t -> Maybe t
 
 -- | 'Type' is an instance of 'WithU', with associated type 'UType'.
 instance WithU Type where
   type U Type = UType
   toU = unfreeze
-  fromU = fromJust . freeze
+  fromU = freeze
 
 -- | A 'WithU' instance can be lifted through any functor (including,
 --   in particular, 'Ctx' and 'Poly').
-instance (WithU t, Functor f) => WithU (f t) where
+instance (WithU t, Traversable f) => WithU (f t) where
   type U (f t) = f (U t)
   toU = fmap toU
-  fromU = fmap fromU
+  fromU = traverse fromU
 
 ------------------------------------------------------------
 -- Pattern synonyms