diff --git a/src/Cornelis/Pretty.hs b/src/Cornelis/Pretty.hs
index 0600e3c..9130ceb 100644
--- a/src/Cornelis/Pretty.hs
+++ b/src/Cornelis/Pretty.hs
@@ -176,6 +176,11 @@ prettyGoals (InferredType ty) =
 prettyGoals (WhyInScope msg) = pretty msg
 prettyGoals (NormalForm expr) = pretty expr
 prettyGoals (DisplayError err) = annotate CornelisError $ pretty err
+prettyGoals (IntroConstructorUnknown constructors) = vsep
+  [ annotate CornelisErrorWarning "Don't know which constructor to introduce."
+  , mempty
+  , section "Constructors available" constructors prettyName
+  ]
 prettyGoals (UnknownDisplayInfo v) = annotate CornelisError $ pretty $ show v
 
 prettyInterval :: AgdaInterval -> Doc HighlightGroup
diff --git a/src/Cornelis/Types.hs b/src/Cornelis/Types.hs
index bfea1dc..59e356b 100644
--- a/src/Cornelis/Types.hs
+++ b/src/Cornelis/Types.hs
@@ -314,6 +314,7 @@ data DisplayInfo
   | HelperFunction Text
   | InferredType Type
   | DisplayError Text
+  | IntroConstructorUnknown [Text]
   | WhyInScope Text
   | NormalForm Text
   | UnknownDisplayInfo Value
@@ -339,6 +340,7 @@ instance FromJSON DisplayInfo where
       "Error" ->
         obj .: "error" >>= \err ->
           DisplayError <$> err .: "message"
+      "IntroConstructorUnknown" -> IntroConstructorUnknown <$> obj .: "constructors"
       "InferredType" ->
         InferredType <$> obj .: "expr"
       "WhyInScope" ->