Type level programming: Dealing with ambiguous type error

jaror:

No, matching on types is not (and should not be) possible even with full dependent types like in Agda. I hope this is not a planned feature.

Sorry, I meant foreach, not forall ->. (forall -> is RequiredTypeArguments!) Does that resolve the confusion?

I believe “foreach” corresponds to a “Pi-type” or “dependent product” in dependent type theory, and should be possible in Agda, as far as I know. In Haskell it boils down to something like passing Typeable or the singleton for the type in question.

You can see a little more in the Dependent Products section of the Serokell Dependent Types roadmap.

EDIT: I see from your edit that it was a conceptual example of using foreach in a future version of GHC. In the meantime

I’m not sure whether your example was supposed to be literal or conceptual but here’s a literal version that uses a hand-written singleton:

{-# LANGUAGE GHC2024 #-}

import Data.Kind

data SMyType t where
  STInt :: SMyType Int
  STBool :: SMyType Bool

negateLike :: forall (t :: Type). SMyType t -> t -> t
negateLike STInt x = -x
negateLike STBool x = not x