This works mostly but I've got a problem stuffing a TcCoercion into a PostTc id Coercion.
See Trac #10803
Here's how it currently behaves:
λ:11> :t (:: Maybe ()) (:: Maybe ()) :: Maybe () -> Maybe () λ:12> :t (:: a) (:: a) :: (forall a. a) -> forall a. a -- ^^ I'm not happy with this one above λ:15> :t (show . (:: Int) . read) (show . (:: Int) . read) :: String -> String λ:16> (show . (:: Int) . read) " 00123123123" "123123123" it :: String λ:17> :t length length :: Foldable t => t a -> Int λ:18> :t length . (:: [Int]) length . (:: [Int]) :: [Int] -> Int λ:19> :t length . (:: [a]) <interactive>:1:11: error: Couldn't match type ‘forall a1. [a1]’ with ‘t0 a0’ Expected type: a -> t0 a0 Actual type: (forall a. [a]) -> forall a. [a] In the second argument of ‘(.)’, namely ‘(:: [a])’ In the expression: length . (:: [a]) -- ^^ again, I'm not happy with this last one... λ:21> (:: [_]) ("Hello" :: String) <interactive>:21:6: error: Found type wildcard ‘_’ standing for ‘Char’ To use the inferred type, enable PartialTypeSignatures Relevant bindings include it :: [Char] (bound at <interactive>:21:1) In an expression type signature: [_] In the expression: :: [_] In the expression: (:: [_]) ("Hello" :: String) λ:22> (:: [a]) ("Hello" :: String) <interactive>:22:11: error: Couldn't match type ‘a1’ with ‘Char’ ‘a1’ is a rigid type variable bound by a type expected by the context: [a1] at <interactive>:22:1 Expected type: [a1] Actual type: String In the first argument of ‘:: [a]’, namely ‘("Hello" :: String)’ In the expression: (:: [a]) ("Hello" :: String) In an equation for ‘it’: it = (:: [a]) ("Hello" :: String) -- ^^ :-(
I'm not even sure why I need the coercion at all though... :-)
Here's the constructur signature:
data HsExpr id = -- ... | TySigSectionOut (LHsType Name) (PostTc id Type) (PostTc id Coercion)
I've noticed there's a
dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
operation, but this only works in the DsM monad, however, if I use a PostTc id TcCoercion for the field instead, I get deriving problems with the Data instance for HsExpr...
The examples involving type variables are odd. They should probably be generalized as part of the type ascribed to the function, and not as the argument. I.E. right now we have:
(:: type) = \(x :: Generalize[type]) -> x
but we want something more like:
(:: type) = ((\(x :: type) -> x) :: Generalize[type -> type])
Is there a wiki page for this proposal?
I agree that (:: a) :: (forall a. a) -> (forall a. a) is a bit strange. Note that if a were in scope, this generalization wouldn't happen. What is a use-case for using a not-in-scope type variable in a signature section? Perhaps the programmer would prefer a type wildcard instead (which should work out of the box, I think)? So maybe this isn't so bad, after all.
Would there be any runtime consequences of using this feature? Naively, it would seem so, as we're creating a new function and calling it. That would make me sad.
I think I agree with Richard. I can't think of a reason to use (unbound) variables other than for them to work as wildcards. But we have wildcards. So perhaps the current behavior is okay, or should be an error, rather than what I suggested.
As for performance, assuming this did just turn into \(x :: ty) -> x, wouldn't the optimizer eliminate it?
While trying out the implementation I was wondering if we don't want
to be mostly syntactic shorthand for the typed lambda abstraction
(\ ( x :: <type> ) -> x )
Allowing for things like (:: (a,a)) to mean
> :set -XScopedTypeVariables > :t (\(x::(a,a)) -> x) (\(x::(a,a)) -> x) :: (a, a) -> (a, a)
or things like (:: Exception e => Either e a) which can't be done with wildcards right now (as we don't have named wildcards at the type-level afaik).
Are we sure this would always happen? What if we end up mapping the signature section? Or do other strange things with it? In any case, this should be tested.
Would we enable -XScopedTypeVariables locally over the signature section? (I think we should, under this proposal.) But I actually prefer the wildcards approach. Note that, under the current implementation of ScopedTypeVariables, a scoped type variable may unify only with a variable never a known type. (For example, (\(x :: (a,a)) -> x) (True, False) does not type-check.) Also, with wildcards, the user can get feedback about what the correct type should be.
And, yes, I do believe we have named type wildcards, so your case with a repeated variable should be OK.
You're right! I forgot they need to be enabled separately via -XNamedWildCards. Also, Lennart is ok with not supporting free variables and doing a conservative implementation for now which can be extended later, his response to me was (assuming he's ok with me quoting him here) :
I'd say, make it as conservative as possible.
So I'd ban free type variables in the type. It's a restriction that can be relaxed if we want.
But I'm happy if you give it some other sensible semantics.
I'm not sure I understand what you're asking. No, map id isn't (in general) free, and neither is it if you replace id with a signature section. If these are expected to behave like first-class functions, then when used as such, there are potentially costs, just like there are with id.
Or are you worried that they are more costly than id?
Please make a wiki page to describe the design. There are, as you have discovered, always wrinkles.
I strongly agree (for now anyway) we should only allow a named type variable (like 'a') in a signature section if 'a' is lexically in scope from some enclosing construct. No implicit quantification! If you want wildcards use wildcards.
I have not yet looked at the code. Let's get the design agreed first.
Thanks for doing this.
Signature sections might be worse than id in at least two ways: 1) there might be RULES around id that wouldn't apply, and 2) a signature section would seem to allocate a new function instead of using an existing one. Both of these issues would be mitigated if (:: t) expanded to (id @t), where @t is a visible type application (see D1138).
But, to be honest, I'm not all that worried about being worse than id. I'm worried about being worse than a normal type signature -- that is, to have any runtime cost at all. Signature sections are meant as a light syntactic sugar, and they have appeal as such. But I would avoid them entirely if this light syntactic sugar cost me at runtime.
While I'm thinking about visible type application, once we have that feature, is this one needed any more? Do we have real-ish examples of when we want signature sections? The examples for http://augustss.blogspot.co.at/2014/04/a-small-haskell-extension.html are all quite easy to write with visible type application.