module Quals () where

data G = G { gx :: Int, gy :: Int }


-- | We should scrape qualifiers from data definitions; why doesn't it happen
--   "automatically" from the data-con-function signature anyway?

{-@ data G = G { gx :: Int, gy :: {v:Int | v = gx + 5} } @-}

poo :: Int -> Int
poo n = n + 5

-- | `goo` fails because `poo` doesn't have the type `n -> n + 5` because no qual...

{-@ goo :: {v:Int | v = 105} @-}
goo :: Int
goo = poo 100

-- | But `goo` succeeds if we add `chump` into the mix, because
--   it picks up the qualifers.

{- chump :: z:Int -> {v:Int | v = z + 5} @-}
chump   :: Int -> Int
chump z = z + 5