module T433 where

import Data.Kind (Type)
import Data.Singletons.Base.TH
import Prelude.Singletons

$(promote [d|
  konst1 :: a -> Bool -> a
  konst1 x _ = x

  konst2 :: a -> Maybe Bool -> a
  konst2 x _ = x

  f local = g
    where
      g :: forall a. a -> a
      g x = konst1 (x :: a) local

  foo :: forall a. a -> ()
  foo x = const () (Nothing :: Maybe a)

  id2 :: forall a. a -> a
  id2 x = id (x :: a)

  id3 :: a -> a
  id3 (x :: b) = id (x :: b)

  id4 :: forall a. a -> a
  id4 (x :: a) = id (x :: a)

  id5 :: forall a. a -> a
  id5 = g
    where
      g = id :: a -> a

  id6 :: a -> a
  id6 (x :: b) = g
    where
      g = (x :: b)

  id7 (x :: b) = g
    where
      g = (x :: b)

  id8 :: a -> a
  id8 x = g x True
    where
      g :: b -> a -> b
      g y _ = y

  -- These version will not work. See the singletons README for more about these
  -- limitations.

  -- This will not work because the `a` in `forall a` scopes over the body of
  -- the function, but the `(x :: b)` pattern refers to `b` instead of `a`.
  {-
  id9 :: forall a. a -> a
  id9 (x :: b) = id (x :: b)
  -}

  -- This will not work because the `b` in `Nothing :: Maybe b` is bound by the
  -- type signature for `g`, a local variable that closes over `x`. Moreover,
  -- `b` is only mentioned in the return type (and not the arguments) of the
  -- type signature.
  {-
  id10 :: forall a. a -> a
  id10 x = konst2 x y
    where
      y :: forall b. Maybe b
      y = Nothing :: Maybe b
  -}
  |])