In many cases I find myself wanting to emulate e.g. Idris’s {x : A} syntax, albeit it seems to me that this isn’t possible in general in Haskell.
For functions, you can add a forall.
For data and newtype, you can use GADT-syntax.
E.g.
-- I use a variant of this in production
newtype Cont :: forall (r :: Type). Type -> Type where
Cont :: forall r a. {runCont :: ((a -> r) -> r)} -> Cont @r a
What can be done for type families and/or type synonyms?
I can’t seem to do anything like the following
-- There doesn't seem to be a syntax for this?
type SomeIdentity {a} = Identity a
-- `x` isn't in scope, and even then, arity mismatch I assume
type family SomeIdentity' :: forall (x :: Type). Type where
SomeIdentity' = Identity x
Thanks! I’ve been searching for a solution for this for quite some time. I wish it were better documented somewhere.
There are unfortunately still some weird issues, but at least I can do it now:
import Data.Kind (Type)
type SomeType :: forall a. Type
type family SomeType where
SomeType @a = a
x :: forall a. SomeType @a
x = error "undefined"
y :: forall a. a
y = x -- @a
I get the following error if I remove @a:
Test.hs:11:5: warning: [-Wdeferred-type-errors]
• Couldn't match expected type ‘a’ with actual type ‘SomeType’
‘a’ is a rigid type variable bound by
the type signature for:
y :: forall a. a
at Test.hs:10:1-16
• In the expression: x
In an equation for ‘y’: y = x
• Relevant bindings include y :: a (bound at Test.hs:11:1)
|
11 | y = x
| ^