Explicit implicit type parameters for type families?

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

Is there any way to do this with type families?

1 Like

I believe the @ty syntax will get you what you want. If I change @Bool in the following, I get a type error:

type Foo :: forall a b c. b -> c
type family Foo b where
  Foo @Int @Bool True = Bool

This is only for invisible matches, and you have to add a formal to declare the ordering if you want to match.

1 Like

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
   |     ^

Using @_ gives the same error.

If you make the type family take an explicit input instead, inference works fine for some reason.