File tree Expand file tree Collapse file tree 3 files changed +16
-2
lines changed Expand file tree Collapse file tree 3 files changed +16
-2
lines changed Original file line number Diff line number Diff line change @@ -129,8 +129,6 @@ compileType t = do
129129 x <- hsName <$> compileDBVar x
130130 return $ tApp (Hs. TyVar () x) vs
131131
132- Sort s -> return (Hs. TyStar () )
133-
134132 Lam argInfo restAbs -> do
135133 (body , x0) <- underAbstraction_ restAbs $ \ b ->
136134 (,) <$> compileType b <*> (hsName <$> compileDBVar 0 )
Original file line number Diff line number Diff line change 1+ module Fail.Issue449 where
2+
3+ open import Haskell.Prelude
4+
5+ foo : Set → Int
6+ foo _ = 42
7+ {-# COMPILE AGDA2HS foo #-}
8+
9+ goo : ∀ {a : Set₁ } → (a → Int) → Bool
10+ goo _ = True
11+ {-# COMPILE AGDA2HS goo #-}
12+
13+ test = goo foo
14+ {-# COMPILE AGDA2HS test #-}
Original file line number Diff line number Diff line change 1+ test/Fail/Issue449.agda:13.1-5: error: [CustomBackendError]
2+ agda2hs: Bad Haskell type: Type
You can’t perform that action at this time.
0 commit comments