Make DomForall's argument optional to represent implicit foralls

Author: zeroeightysix

src/Agda2Hs/Compile/ClassInstance.hs

@@ -115,12 +115,14 @@ compileInstRule xs cs ty = do
             pars t@(Hs.TyCon () _) = t
             pars t = Hs.TyParen () t
     Pi a b -> compileDomType (absName b) a >>= \case
-      DomDropped -> underAbstr a b (compileInstRule xs cs . unEl)
+      DomDropped -> underAbstr a b skip
       DomConstraint hsA ->
         underAbstraction a b (compileInstRule xs (cs ++ [hsA]) . unEl)
       DomType _ t -> __IMPOSSIBLE__
-      DomForall x ->
+      DomForall Nothing -> underAbstr a b skip
+      DomForall (Just x) ->
         underAbstraction a b (compileInstRule (xs ++ [x]) cs . unEl)
+      where skip = compileInstRule xs cs . unEl
     _ -> __IMPOSSIBLE__
 
 

src/Agda2Hs/Compile/Data.hs

@@ -81,12 +81,14 @@ compileConstructor params c = do
 compileConstructorArgs :: Telescope -> C [Hs.Type ()]
 compileConstructorArgs EmptyTel = return []
 compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \case
-  DomType s hsA     -> do
+  DomType s hsA      -> do
     ty <- addTyBang s hsA
     (ty :) <$> underAbstraction a tel compileConstructorArgs
-  DomConstraint hsA -> agda2hsError "Not supported: constructors with class constraints"
-  DomDropped        -> underAbstraction a tel compileConstructorArgs
-  DomForall{}       -> __IMPOSSIBLE__
+  DomConstraint hsA  -> agda2hsError "Not supported: constructors with class constraints"
+  DomDropped         -> skip
+  DomForall Nothing  -> skip
+  DomForall (Just _) -> __IMPOSSIBLE__
+  where skip = underAbstraction a tel compileConstructorArgs
 
 checkCompileToDataPragma :: Definition -> String -> C ()
 checkCompileToDataPragma def s = noCheckNames $ do

src/Agda2Hs/Compile/Function.hs

@@ -177,7 +177,8 @@ compileModuleParams (ExtendTel a tel) = do
   (f , p) <- compileDomType (absName tel) a >>= \case
     DomDropped -> return (id, [])
     DomConstraint c -> return (constrainType c, [])
-    DomForall a -> return (qualifyType a, [])
+    DomForall Nothing -> return (id, [])
+    DomForall (Just a) -> return (qualifyType a, [])
     DomType s a -> do
       let n = hsName $ absName tel
       checkValidVarName n

src/Agda2Hs/Compile/Record.hs

@@ -166,7 +166,8 @@ compileRecord target def = do
             ToRecord{} -> agda2hsError $
               "Not supported: record/class with constraint fields"
           DomDropped -> return (hsAssts , hsFields)
-          DomForall{} -> __IMPOSSIBLE__
+          DomForall Nothing -> return (hsAssts , hsFields)
+          DomForall (Just _) -> __IMPOSSIBLE__
       (_, _) -> __IMPOSSIBLE__
 
     compileDataRecord

src/Agda2Hs/Compile/Type.hs

@@ -101,7 +101,8 @@ compileType t = do
         DomType _ hsA -> Hs.TyFun () hsA <$> compileB
         DomConstraint hsA -> constrainType hsA <$> compileB
         DomDropped -> compileB
-        DomForall hsA -> qualifyType hsA <$> compileB
+        DomForall Nothing -> compileB
+        DomForall (Just hsA) -> qualifyType hsA <$> compileB
 
     Def f es -> maybeUnfoldCopy f es compileType $ \f es -> do
       def <- getConstInfo f
@@ -243,11 +244,12 @@ compileDomType x a =
         | isNested -> do
           tellExtension Hs.RankNTypes
           -- tellExtension Hs.ExistentialQuantification
-          return $ DomForall $ Hs.UnkindedVar () $ Hs.Ident () x
+          return $ DomForall $ Just $ Hs.UnkindedVar () $ Hs.Ident () x
         | ctx < npars -> do
           tellExtension Hs.ScopedTypeVariables
-          return $ DomForall $ Hs.UnkindedVar () $ Hs.Ident () x
-        | otherwise -> return DomDropped
+          return $ DomForall $ Just $ Hs.UnkindedVar () $ Hs.Ident () x
+        -- Return an implicit forall.
+        | otherwise -> return $ DomForall Nothing
     DOTerm     -> fmap (uncurry DomType) . withNestedType . compileTypeWithStrictness . unEl $ unDom a
 
 compileTeleBinds :: Bool -> Telescope -> C [Hs.TyVarBind ()]

src/Agda2Hs/Compile/Types.hs

@@ -205,8 +205,8 @@ data CompiledDom
     -- ^ To a Haskell type (with perhaps a strictness annotation)
   | DomConstraint (Hs.Asst ())
     -- ^ To a typeclass constraint
-  | DomForall (Hs.TyVarBind ())
-    -- ^ To an explicit forall
+  | DomForall (Maybe (Hs.TyVarBind ()))
+    -- ^ To a forall, with an optional type variable declaration. If Nothing, this is an implicit forall; otherwise, explicit.
   | DomDropped
     -- ^ To nothing (e.g. erased proofs)