Skip to content

Commit

Permalink
Implement partial support for promoting scoped type variables
Browse files Browse the repository at this point in the history
`singletons-th` can now promote a good number of uses of scoped type variables,
save for the two exceptions now listed in the `singletons` `README`. This is
accomplished by a combination of:

1. Bringing scoped type variables into scope on the left-hand sides of promoted
   type family equations through invisible `@` arguments when a function uses
   an outermost `forall` in its type signature (and does not close over any
   local variables).

2. Bringing scoped type variables into scope on the left-hand sides of promoted
   type family equations through explicit kind annotations on each of the type
   family's arguments when a function has an outermost `forall` in its type
   signature.

3. Closing over scoped type variables when lambda-lifting to ensure that the
   type variables are accessible when scoping over local definitions.

See the new `Note [Scoped type variables]` in
`Data.Singletons.TH.Promote.Monad` for more about how this is implemented.

Fixes #433.
  • Loading branch information
RyanGlScott committed Aug 26, 2023
1 parent f912f5a commit a61bb77
Showing 17 changed files with 1,037 additions and 195 deletions.
168 changes: 127 additions & 41 deletions README.md
Original file line number Diff line number Diff line change
@@ -839,6 +839,7 @@ The following constructs are fully supported:

The following constructs are partially supported:

* scoped type variables
* `deriving`
* finite arithmetic sequences
* records
@@ -850,6 +851,132 @@ The following constructs are partially supported:

See the following sections for more details.

### Scoped type variables

`singletons-th` makes an effort to track scoped type variables during promotion
so that they "just work". For instance, this function:

```hs
f :: forall a. a -> a
f x = (x :: a)
```

Will be promoted to the following type family:

```hs
type F :: forall a. a -> a
type family F x where
F @a x = (x :: a)
```

Note the use of `@a` on the left-hand side of the type family equation, which
ensures that `a` is in scope on the right-hand side. This also works for local
definitions, so this:

```hs
f :: forall a. a -> a
f x = g
where
g = (x :: a)
```

Will promote to the following type families:

```hs
type F :: forall a. a -> a
type family F x where
F @a x = LetG a x

type family LetG a x where
LetG a x = (x :: a)
```

Note that `LetG` includes both `a` and `x` as arguments to ensure that they are
in scope on the right-hand side.

Besides `forall`s in type signatures, scoped type variables can also come
from pattern signatures. For example, this will also work:

```hs
f (x :: a) = g
where
g = (x :: a)
```

Not all forms of scoped type variables are currently supported:

* If a type signature brings a type variable into scope over the body of a
function with a `forall`, then any pattern signatures must consistently use
the same type variable in argument types that mention it. For example, while
this will work:

```hs
f :: forall a. a -> a
f (x :: a) = a -- (x :: a) mentions the same type variable `a` from the type signature
```

The following will _not_ work:

```hs
f' :: forall a. a -> a
f' (x :: b) = b -- BAD: (x :: b) mentions `b` instead of `a`
```

This is because `singletons-th` would attempt to promote `f'` to the
following:

```hs
type F' :: forall a. a -> a
type family F' x where
F' @a (x :: b) = b
```

And GHC will not infer that `b` should stand for `a`.

* There is limited support for local variables that themselves bring type
variables into scope with `forall`s in their type signatures. For example,
this example works:

```hs
f local = g
where
g :: forall a. a -> a
g x = const (x :: a) local
```

This is because `f` and `g` will be promoted like so:

```hs
type family F local where
F local = G local

type family G local x where
G local (x :: a) = Const (x :: a) local
```

It is not straightforward to give `G` a standalone kind signature, and
without a standalone kind signature, GHC will not allow writing `@a` on the
left-hand side of `G`'s type family equation. On the other hand, we can still
ensure that `a` is brought into scope by writing `(x :: a)` instead of `x` on
the left-hand side. While the `:: a` signature was not present in the
original definition, we include it anyway during promotion to ensure that
definitions like `G` kind-check.

This trick only works if the scoped type variable is mentioned in one of the
local definition's arguments, however. If the scoped type variable is only
mentioned in the return type, then the promoted definition will not
kind-check. This means that examples like this one will not work:

```hs
konst :: a -> Maybe Bool -> a
konst x _ = x

f x = konst x y
where
y :: forall b. Maybe b
y = Nothing :: Maybe b
```

### `deriving`

`singletons-th` is slightly more conservative with respect to `deriving` than
@@ -1304,7 +1431,6 @@ underyling pattern instead.

The following constructs are either unsupported or almost never work:

* scoped type variables
* datatypes that store arrows or `Symbol`
* rank-n types
* promoting `TypeRep`s
@@ -1315,46 +1441,6 @@ The following constructs are either unsupported or almost never work:

See the following sections for more details.

### Scoped type variables

Promoting functions that rely on the behavior of `ScopedTypeVariables` is very
tricky—see
[this GitHub issue](https://github.com/goldfirere/singletons/issues/433) for an
extended discussion on the topic. This is not to say that promoting functions
that rely on `ScopedTypeVariables` is guaranteed to fail, but it is rather
fragile. To demonstrate how fragile this is, note that the following function
will promote successfully:

```hs
f :: forall a. a -> a
f x = id x :: a
```

But this one will not:

```hs
g :: forall a. a -> a
g x = id (x :: a)
```

There are usually workarounds one can use instead of `ScopedTypeVariables`:

1. Use pattern signatures:

```hs
g :: forall a. a -> a
g (x :: a) = id (x :: a)
```
2. Use local definitions:

```hs
g :: forall a. a -> a
g x = id' a
where
id' :: a -> a
id' x = x
```

### Arrows, `Symbol`, and literals

As described in the promotion paper, automatic promotion of datatypes that
1 change: 1 addition & 0 deletions singletons-base/tests/SingletonsBaseTestSuite.hs
Original file line number Diff line number Diff line change
@@ -132,6 +132,7 @@ tests =
, compileAndDumpStdTest "T410"
, compileAndDumpStdTest "T412"
, compileAndDumpStdTest "T414"
, compileAndDumpStdTest "T433"
, compileAndDumpStdTest "T443"
, afterSingletonsNat .
compileAndDumpStdTest "T445"
Original file line number Diff line number Diff line change
@@ -69,28 +69,36 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
Lambda_0123456789876543210Sym3 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210
type family Case_0123456789876543210 x0123456789876543210 t where
Case_0123456789876543210 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 y) x) y
data Let0123456789876543210ZSym0 y0123456789876543210
data Let0123456789876543210ZSym0 a0123456789876543210
where
Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) =>
Let0123456789876543210ZSym0 y0123456789876543210
type instance Apply Let0123456789876543210ZSym0 y0123456789876543210 = Let0123456789876543210ZSym1 y0123456789876543210
Let0123456789876543210ZSym0 a0123456789876543210
type instance Apply Let0123456789876543210ZSym0 a0123456789876543210 = Let0123456789876543210ZSym1 a0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210ZSym0KindInference ())
data Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210
data Let0123456789876543210ZSym1 a0123456789876543210 y0123456789876543210
where
Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 y0123456789876543210) arg) (Let0123456789876543210ZSym2 y0123456789876543210 arg) =>
Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210
type instance Apply (Let0123456789876543210ZSym1 y0123456789876543210) x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 y0123456789876543210) where
Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 a0123456789876543210) arg) (Let0123456789876543210ZSym2 a0123456789876543210 arg) =>
Let0123456789876543210ZSym1 a0123456789876543210 y0123456789876543210
type instance Apply (Let0123456789876543210ZSym1 a0123456789876543210) y0123456789876543210 = Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210ZSym1KindInference ())
type family Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210
type family Let0123456789876543210Z y0123456789876543210 x0123456789876543210 :: a where
Let0123456789876543210Z y x = y
type family Case_0123456789876543210 x0123456789876543210 t where
Case_0123456789876543210 x y = Let0123456789876543210ZSym2 y x
data Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210 x0123456789876543210
where
Let0123456789876543210ZSym2KindInference :: SameKind (Apply (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) arg) (Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 arg) =>
Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210 x0123456789876543210
type instance Apply (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210ZSym2KindInference ())
type family Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210
type family Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
Let0123456789876543210Z a y x = y
type family Case_0123456789876543210 a0123456789876543210 x0123456789876543210 t where
Case_0123456789876543210 a x y = Let0123456789876543210ZSym3 a y x
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
@@ -223,7 +231,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
Foo5 x = Case_0123456789876543210 x x
type Foo4 :: forall a. a -> a
type family Foo4 (a :: a) :: a where
Foo4 x = Case_0123456789876543210 x x
Foo4 @a (x :: a) = Case_0123456789876543210 a x x
type Foo3 :: a -> b -> a
type family Foo3 (a :: a) (a :: b) :: a where
Foo3 a b = Case_0123456789876543210 a b (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a b)
@@ -262,11 +270,11 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
sY)
sFoo4 (sX :: Sing x)
= id
@(Sing (Case_0123456789876543210 x x))
@(Sing (Case_0123456789876543210 a x x))
(case sX of
(sY :: Sing y)
-> let
sZ :: (Sing (Let0123456789876543210ZSym2 y x :: a) :: Type)
sZ :: (Sing (Let0123456789876543210ZSym3 a y x :: a) :: Type)
sZ = sY
in sZ)
sFoo3 (sA :: Sing a) (sB :: Sing b)
Original file line number Diff line number Diff line change
@@ -233,18 +233,26 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
Let0123456789876543210Y x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x)
type family Let0123456789876543210X_0123456789876543210 x0123456789876543210 where
Let0123456789876543210X_0123456789876543210 x = Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x
data Let0123456789876543210BarSym0 x0123456789876543210
data Let0123456789876543210BarSym0 a0123456789876543210
where
Let0123456789876543210BarSym0KindInference :: SameKind (Apply Let0123456789876543210BarSym0 arg) (Let0123456789876543210BarSym1 arg) =>
Let0123456789876543210BarSym0 x0123456789876543210
type instance Apply Let0123456789876543210BarSym0 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210
Let0123456789876543210BarSym0 a0123456789876543210
type instance Apply Let0123456789876543210BarSym0 a0123456789876543210 = Let0123456789876543210BarSym1 a0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210BarSym0 where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210BarSym0KindInference ())
type family Let0123456789876543210BarSym1 x0123456789876543210 :: a0123456789876543210 where
Let0123456789876543210BarSym1 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210
type family Let0123456789876543210Bar x0123456789876543210 :: a where
Let0123456789876543210Bar x = x
data Let0123456789876543210BarSym1 a0123456789876543210 x0123456789876543210
where
Let0123456789876543210BarSym1KindInference :: SameKind (Apply (Let0123456789876543210BarSym1 a0123456789876543210) arg) (Let0123456789876543210BarSym2 a0123456789876543210 arg) =>
Let0123456789876543210BarSym1 a0123456789876543210 x0123456789876543210
type instance Apply (Let0123456789876543210BarSym1 a0123456789876543210) x0123456789876543210 = Let0123456789876543210Bar a0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210BarSym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210BarSym1KindInference ())
type family Let0123456789876543210BarSym2 a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
Let0123456789876543210BarSym2 a0123456789876543210 x0123456789876543210 = Let0123456789876543210Bar a0123456789876543210 x0123456789876543210
type family Let0123456789876543210Bar a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
Let0123456789876543210Bar a x = x
data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210
where
(:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) arg) =>
@@ -726,7 +734,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
Foo13_ y = y
type Foo13 :: forall a. a -> a
type family Foo13 (a :: a) :: a where
Foo13 x = Apply Foo13_Sym0 (Let0123456789876543210BarSym1 x)
Foo13 @a (x :: a) = Apply Foo13_Sym0 (Let0123456789876543210BarSym2 a x)
type Foo12 :: Nat -> Nat
type family Foo12 (a :: Nat) :: Nat where
Foo12 x = Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) x) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))
@@ -832,7 +840,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
sFoo13_ (sY :: Sing y) = sY
sFoo13 (sX :: Sing x)
= let
sBar :: (Sing (Let0123456789876543210BarSym1 x :: a) :: Type)
sBar :: (Sing (Let0123456789876543210BarSym2 a x :: a) :: Type)
sBar = sX
in applySing (singFun1 @Foo13_Sym0 sFoo13_) sBar
sFoo12 (sX :: Sing x)
Original file line number Diff line number Diff line change
@@ -46,10 +46,10 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations
Field1Sym1 a0123456789876543210 = Field1 a0123456789876543210
type Field2 :: forall a. Record a -> Bool
type family Field2 (a :: Record a) :: Bool where
Field2 (MkRecord _ field) = field
Field2 @a (MkRecord _ field :: Record a) = field
type Field1 :: forall a. Record a -> a
type family Field1 (a :: Record a) :: a where
Field1 (MkRecord field _) = field
Field1 @a (MkRecord field _ :: Record a) = field
sField2 ::
forall a (t :: Record a). Sing t
-> Sing (Apply Field2Sym0 t :: Bool)
Loading

0 comments on commit a61bb77

Please sign in to comment.