ScopedTypeVariables could allow more programs

changed milestone to %8.6.1

changed weight to 5

added Tfeature request Trac import labels

This is a consequence of the fact that a scoped type variable must be a variable, never a type. Another way of saying this is that a type variable brought into scope in a pattern type annotation simply names an existing type variable; it can't, say, bind a type variable to a type.

Of course, with type equalities (and therefore GADTs), you can have a type variable a and the constraint a ~ Int. In this case, you can bind a scoped type variable to a, despite the equality constraint saying that you're essentially binding a scoped type variable to a type.

I've personally never liked this design choice around scoped type variables, believing that a pattern-bound type variable should be able to be bound to any type. The lack of ability to do this has actually been a pain point in singletons from the beginning, and these examples show that the current behavior isn't even truly self-consistent.

Another layer of inconsistency can be found between values and types. GHC accepts this:

data T a where
  MkT :: Bool -> T Bool

f :: T a -> a
f (MkT (y :: z)) = y

But not this:

type family F (t :: T a) :: a where
  F (MkT (y :: z)) = y

    • Expected kind ‘Bool’, but ‘(y :: z)’ has kind ‘z’
    • In the first argument of ‘MkT’, namely ‘(y :: z)’
      In the first argument of ‘F’, namely ‘(MkT (y :: z))’
      In the type family declaration for ‘F’

I think ticket:15050#comment:152119 is a red herring. You're right that GHC rejects that type family, but that has more to do with the way that GHC does type-level GADT pattern matching than anything with scoped type variables. You could argue that it's suboptimal (though it matches what Agda does, I believe), but it's a separate matter from this ticket, I believe.

This is a consequence of the fact that a scoped type variable must be a variable, never a type. Another way of saying this is that a type variable brought into scope in a pattern type annotation simply names an existing type variable; it can't, say, bind a type variable to a type.

TBH, I don’t understand that part of the docs for ScopedTypeVariables. What does it mean for a type variable to be a type variable? Is there a global set of variables in existing? Is it referring to the variables in the signature of of the constructor? … I guess the latter could be, but I agree with your sentiment that that is pretty odd and unsatisfying, especially given the type variables in the type signature of the constructor are not in scope here.

What does it mean for a type variable to be a type variable?

Imagine the fully-typechecked Core program. Now, does the source-level type variable name a type variable, or some other non-type-variable type? Example:

data T a = MkT a

f1 :: T b -> Int
f1 (MkT (x::z)) = ...   -- OK

f2 :: T Boll -> Int
f2 (MkT (x::z)) = ...   -- Not OK

In f1 the source-level lexical type variable z names a type variable in Core. The elaborated version of f1 could be

f1 = /\b. \(x::T b). case x of { MkT (x::b) -> ... }

So z names b.

In f2, you'll see that z names Int.

I agree this is a questionable choice. At the time I was worried that it'd be confusing to have a type variable that was just an alias for Int; that is not a type variable at all. But in these days of GADTs and type equalities we are all used to that. We'd make a different choice today.

Feel free to make a GHC proposal to change this behaviour. It'd be backward compatible!

Imagine the fully-typechecked Core program.

That’s an unsatisfying way to explain a Haskell feature :-)

Feel free to make a GHC proposal to change this behaviour. It'd be backward compatible!

Is there someone who is confident about type-checker features that feels inspired to turn this into a proposal? (Richard? :-)) I still feel mostly like a clueless user with a too strong sense of entitlement…

But I can give it a shot, of course.

I've got enough proposals in the air right now. :)

So I'll pass the buck: Ryan?

Nope. I have a personal policy that I never make a GHC proposal unless I understand how it would be implemented in GHC and would be willing to implement it myself, and I don't meet these criteria. Nor am I particularly eager to dive into this part of the codebase—typechecking scoped type variables is black magic, and I'm content to let the experts handle it.

Here is another case where ScopedTypeVariables are less powerful than one might expect. This works:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

type family F a where F Bool = Int

data T a where MkT :: forall b a. b ~ F a => b -> T a
foo :: T Bool -> ()
foo (MkT (_ :: Int)) = ()

but the equivalent(?) formulation using TypeFamilies does not:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

class C b a | a -> b
instance C Int Bool
data T a where MkT :: forall b a. C b a => b -> T a
foo :: T Bool -> ()
foo (MkT (_ :: Int)) = ()

gives

/tmp/Foo.hs:11:11: error:
    • Couldn't match expected type ‘b’ with actual type ‘Int’
      ‘b’ is a rigid type variable bound by
        a pattern with constructor: MkT :: forall b a. C b a => b -> T a,
        in an equation for ‘foo’
        at /tmp/Foo.hs:11:6-19
    • When checking that the pattern signature: Int
        fits the type of its context: b
      In the pattern: _ :: Int
      In the pattern: MkT (_ :: Int)

}}}

mentioned in commit f04ac4d4

I can get the example from the original ticket to work simply by using TauTv instead of SigTv. But I’m sure that breaks stuff – in particular since SigTv are also used for type-checking (see faec8d35 and 8361b2c5) – maybe a separate KindTv would be cleaner?

An experimental implementation of this is in wip/T15050.

Your patch looks fine. Easiest to leave SigTv alone; and just change what sort of tyvar is used in a pattern type signature; which is what you have done.

It's a simple change. Just a question of deciding what we want. I'm ok with binding a type variable to an arbitrary type. GHC proposal?

Easiest to leave SigTv alone; and just change what sort of tyvar is used in a pattern type signature; which is what you have done.

You don't the name to be changed? Good with me.

GHC proposal?

There are so many proposals already … but I guess that’s a good thing :-) Will whip something up.

Proposed at https://github.com/ghc-proposals/ghc-proposals/pull/128

You don't the name to be changed?

Well, not yet. Comments, maybe!

Comments, maybe!

Sure, I will have to go through all of the related notes (which are already partly out-of-date even before my patch). I’ll do that after the proposal process.

changed milestone to %8.8.1

These won't be addressed by GHC 8.6.

I put the current code up for review, but there isn’t really anything to see; I am just changing one function call :-)

Trac metadata

Trac field	Value
Differential revisions	- → D4980

mentioned in commit 4d91cabc

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

mentioned in issue #15480 (closed)

Thanks, nomeata! Do you think you could add a mention of this new feature in the 8.8.1 release notes?

mentioned in commit f811685c

mentioned in commit a50244c6

Links

GHC proposal
GHC proposal discussion
paper (Type variables in patterns)

marked this issue as related to #15119 (closed)

added Pnormal label

added ScopedTypeVariables label

mentioned in issue #18591

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

ScopedTypeVariables could allow more programs

Child items ...

Activity

ScopedTypeVariables could allow more programs

Relates to

Activity