-
Notifications
You must be signed in to change notification settings - Fork 46
Closed
Labels
bugSomething isn't workingSomething isn't working
Milestone
Description
Discovered during my presentation at AIM XLI:
foo : Set → Int
foo _ = 42
{-# COMPILE AGDA2HS foo #-}
goo : ∀ {a : Set₁} → (a → Int) → Bool
goo _ = True
{-# COMPILE AGDA2HS goo #-}
test = goo foo
{-# COMPILE AGDA2HS test #-}This produces the following invalid Haskell:
foo :: Int
foo = 42
goo :: (a -> Int) -> Bool
goo _ = True
test :: Bool
test = goo foo
It should reject the definition of test instead, since the type parameter a should only be instantiated with a valid Haskell type.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working