Thanks!

A few comments:

• I think you need a new clause in unifyTypes.
• I would prefer to not overload the type constructor notation, since it's not a regular type constructor, and to use something like a keyword instead, such as proxy T.

• Ok
• I agree

A couple more thoughts:

• Don't forget to update the types pretty printer in Docs/Publish, otherwise Pursuit will crash on any modules containing proxy types.
• Perhaps RowCons can use proxy to simulate poly kinds now, like @natefaubion has done with FProxy in his polymorphic variants implementation.

Perhaps RowCons can use proxy to simulate poly kinds now, like @natefaubion has done with FProxy in his polymorphic variants implementation.

That was one question I had, whether I could write something like this:

prj
  ∷ ∀ sym f a r1 r2
  . RowCons sym (proxy f) r1 r2
  ⇒ IsSymbol sym
  ⇒ proxy sym
  → VariantF r2 a
  → Maybe (f a)
prj p = on p Just (const Nothing)

Note the use of proxy in RowCons.

That was one question I had, whether I could write something like this:

I think so, because it's not like RowCons uses any value with that type, it's a purely type-level function. So there doesn't need to be an actual polykinded type anywhere.

What was the reason for not using the symbol at the type level too?

Sorry, which symbol again? :)

So it's @"foo" at the value level, but proxy "foo" at the type level currently?

Bump for the @ vs proxy question, I know at least @kritzcreek, @natefaubion, and me don't love that it's different between types and values. 😄

I'm also a bit confused about that, I think it would be nice to use the same syntax for the type and the value if possible.

I'd be fine with @ in types.

I'm fineish with @a being the type syntax for "proxy of a". However, usually, the syntax of a value and the syntax of the type of that value do not coincide. Different things look different. Consistently, @a would be a type of kind proxy a.

I'll change it due to popular demand. We can always change it back. Fun fact: with this change, this PR will no longer be a breaking change.

Travis says

  tests/TestCompiler.hs:218: 
  1) Passing examples 'DuplicateProperties.purs' should compile and run without error
       Error found:
       in module Main
       at /home/travis/build/purescript/purescript/examples/passing/DuplicateProperties.purs line 6, column 1 - line 6, column 55
       
         Type variable proxy is undefined.
       
       while checking the kind of proxy     
                                    ( x :: a
                                    | r     
                                    )       
                                  -> proxy r
       in value declaration subtractX
       
       See https://github.com/purescript/documentation/blob/master/errors/UndefinedTypeVariable.md for more information,
       or to contribute content related to this error.
       
  tests/TestCompiler.hs:218: 
  2) Passing examples 'FunctionalDependencies.purs' should compile and run without error
       Error found:
       in module Main
       at /home/travis/build/purescript/purescript/examples/passing/FunctionalDependencies.purs line 14, column 1 - line 14, column 75
       
         Type variable proxy is undefined.
       
       while checking the kind of Append a b c => proxy a -> proxy b -> proxy c
       in value declaration appendProxy
       
       See https://github.com/purescript/documentation/blob/master/errors/UndefinedTypeVariable.md for more information,
       or to contribute content related to this error.

with this change, this PR will no longer be a breaking change.

I think we should include this in 0.11.5 then, once the tests pass of course.

Isn't it still a breaking change because @ can't be used as an operator? FWIW I think it was always dubious due to @ in patterns.

Yes, actually, that's true. This currently works, for example:

data Test a b = Test a b

infix 4 type Test as @

x :: forall a. a @ a -> a
x (Test a _) = a

Now I guess the question is, would we rather reserve @ as a type operator, or proxy as a type argument name? I would actually lean towards reserving proxy, since we can always pick some other name, but @ seems like it might be handy as a type operator for some things.

Using proxy is "more breaking" than @ given there were numerous examples of its existing usage up there ^, but I don't feel strongly about the syntax for it either way... although I think maybe the fact that a single @ is actually allowed as an operator currently is a bit weird, given that it doesn't work in patterns:

data Test a b = Test a b

infix 4 type Test as @
infix 4 Test as @

x :: forall a. a @ a -> a
x (a @ _) = a -- Type error, Test a0 a0 /~ a0, the compiler sees this as an @ binding, not `Test a _`

Actually, given that, I think I do prefer @. It would be weirder that there's a single reserved lname in the types, vs a magic prefix type operator that is already somewhat-reserved at the value level.

Alright then, @ it is. Thanks!

I guess the above parse does mean you can't use a proxy literal in a pattern, but then you don't really need to since they're singly-inhabited.

@garyb the list of uses of proxy above are values, not types. proxy would only be a keyword in types.

🎆 Thanks!