diff --git a/src/Language/Coq/Deep.hs b/src/Language/Coq/Deep.hs index 8496e95a8a3a47d07580f2c08cdb1cfdc7db6e29..a415a7a1517de943a173dce3fd1292b61917003d 100644 --- a/src/Language/Coq/Deep.hs +++ b/src/Language/Coq/Deep.hs @@ -250,13 +250,16 @@ type SymbolTable = Map.Map Id VTyp -- | Extract the "symbol type" -- --- * if it is a function, the type of the value it returns +-- * if it is a monadic function, the type of the value inside the +-- monad +-- * if it is a non-monadic function, the type of the value it returns -- * if it is a global variable, its type extractSymbolType :: ConversionParams -> Type -> Either ErrorMsg VTyp extractSymbolType _ (Glob ty []) = pure ty extractSymbolType cp typ = go typ where go (Arrow _ ty) = go ty go (Glob m [Glob ty []]) | m == monad cp = pure ty + go (Glob ty []) = pure ty go ty = Left $ impossibleType ty impossibleType ty = "Impossible to extract symbol type of: " ++ show ty