Skip to content

Commit af0b238

Browse files
committed
[ fix #449 ] Set is not a valid Haskell type
1 parent 2286068 commit af0b238

File tree

3 files changed

+16
-2
lines changed

3 files changed

+16
-2
lines changed

src/Agda2Hs/Compile/Type.hs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff 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)

test/Fail/Issue449.agda

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
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 #-}

test/golden/Issue449.err

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
test/Fail/Issue449.agda:13.1-5: error: [CustomBackendError]
2+
agda2hs: Bad Haskell type: Type

0 commit comments

Comments
 (0)