Typecasting using type application syntax

I created #11350 (closed) to allow visible (static) type applications in patterns. I had a thought about translating non-parametric type applications in patterns as a runtime type check (Typeable) and decided to create a ticket in case it made any sense. Example:

doubleWhenInt :: forall a. Typeable a => a -> a
doubleWhenInt x =
  case eqT @Int @a of
    Just Refl -> x + x
    Nothing   -> x

-- Becomes…
doubleWhenInt :: Typeable a => a -> a
doubleWhenInt @Int n = n + n
doubleWhenInt @_   x = x

Thoughts?

Trac metadata

Trac field	Value
Version
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #11350 (closed)

changed weight to 5

added Tfeature request Trac import TypeApplications labels

It would make sense to do something a bit like this.

If a :: * is a type, then a Typeable a constraint is essentially an (invisible) singleton witness to a; the visible singleton is TypeRep a. I think the Right Thing to do would be to get rid of the singleton construction and add pi-types, so that we have

doubleWhenInt :: pi a . a -> a
doubleWhenInt @Int n = n + n
doubleWhenInt @_   x = x

The pi a . quantifier corresponds to forall a . Typeable a =>. The type argument is operationally relevant, can be pattern-matched and hence is non-parametric. The argument would be invisible-by-default (e.g. you might write doubleWhenInt True at a call site) but could be made visible like other type arguments (e.g. doubleWhenInt @Int 42 should be allowed).

(It's not completely obvious whether arguments to pi-quantified functions should be in the type namespace or the term namespace, because they exist at both levels.)

Yes, this is sensible, but I prefer Adam's construction. Yes, the namespace issue is thorny. No, I don't have plans to implement this today. I believe this will be much easier to do after we have pi for non-*-kinded things.

For one thing, pi quantifiers would come in a specific order, while Typeable constraints live in a bag of constraints. What would happen if you have multiple types to match on?

mentioned in issue #11439

added Pnormal label