{-# LANGUAGE TypeApplications, RankNTypes, PolyKinds #-}

module VtaFail1 where

pairup_nosig x y = (x, y)

answer_nosig = pairup_nosig @Int @Bool 5 True

addOne :: Num a => a -> a
addOne x = x + 1

answer_constraint_fail = addOne @Bool 5

answer_lambda = (\x -> x) @Int 12

pair :: forall a. a -> forall b. b -> (a, b)
pair x = (,) x
-- Without this eta-expansion, the two have
-- different types under simple subsumption (#17775)

a = pair 3 @Int @Bool True

data First (a :: * -> *) = F

first :: First a -> Int
first _ = 0

fInt = first @Int F -- should fail

data Proxy (a :: k) = P -- This expands to P (kind variable) (type variable)

foo :: Proxy a -> Int
foo _ = 0

baz = foo @Bool (P :: Proxy Int) -- should fail

data Three (a :: * -> k -> *) = T

too :: Three a -> Int
too _ = 3

threeBad = too @Maybe T
threeWorse = too @( -> ) (T :: Three Either)

plus :: Int -> Int -> Int
plus = (+)

b = plus @Int 5 7
c = plus @Rational 5 10
d = (+) @Int @Int @Int 12 14


e = show @Int @Float (read "5")
f = show (read @Int @Bool @Float "3")

silly :: a -> Bool
silly _ = False

g = silly @Maybe      -- should fail