Opened 10 months ago

Closed 9 months ago

Last modified 9 months ago

#16059 closed bug (fixed)

checkValidType is defeated by a type synonym

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.7
Keywords: Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: typecheck/should_fail/T16059{a,c,d,e}
Blocked By: Blocking:
Related Tickets: Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/112
Wiki Page:

Description

GHC throws an error message on this code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where

f :: forall b (a :: Eq b => b). Int
f = 42
$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20181211: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:6:6: error:
    • Illegal constraint in a kind: Eq b => b
    • In the type signature: f :: forall b (a :: Eq b => b). Int
  |
6 | f :: forall b (a :: Eq b => b). Int
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

However, it does not throw an error message if you hide Eq b => b behind a type synonym, as the following variant of the code above is accepted:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where

type Foo b = Eq b => b

f :: forall b (a :: Foo b). Int
f = 42

Change History (18)

comment:1 Changed 10 months ago by RyanGlScott

The culprit appears to be these lines of check_syn_tc_app:

  = do  { -- See Note [Liberal type synonyms]
        ; liberal <- xoptM LangExt.LiberalTypeSynonyms
        ; if not liberal || isTypeFamilyTyCon tc then
                -- For H98 and synonym families, do check the type args
                mapM_ check_arg tys

          else  -- In the liberal case (only for closed syns), expand then check
          case tcView ty of
             Just ty' -> let syn_tc = fst $ tcRepSplitTyConApp ty
                             err_ctxt = text "In the expansion of type synonym"
                                        <+> quotes (ppr syn_tc)
                         in addErrCtxt err_ctxt $ check_type env ctxt rank ty'
             Nothing  -> pprPanic "check_tau_type" (ppr ty)  }

When checking a type synonym application (like Foo) without LiberalTypeSynonyms enabled, then we don't check the expanded type at all—we only check the arguments! As a consequence, we never validity-check the underlying Eq b => b that is lurking behind the scenes in f :: forall b (a :: Foo b). Int. (This also reveals that enabling LiberalTypeSynonyms will cause the program to be rejected as well.)

comment:2 Changed 10 months ago by simonpj

Huh. Yes, I suppose hat Foo is acceptable in some usage contexts (e.g. as a quantified constraint) but not others (in a kind). So we can't validity-check Foo on its own.

So I suppose we should always validity-check the expansion, tiresome though that is.

Would you like to do that?

The synIsTau field of a SynonymTyCon might allow us to short-circuit the common case where the RHS is totally vanilla. (To do so we'd need to ensure that synIsTau is false if there is a => in the RHS, not just a forall.)

comment:3 in reply to:  2 Changed 10 months ago by RyanGlScott

Replying to simonpj:

So I suppose we should always validity-check the expansion, tiresome though that is.

Would you like to do that?

I tried this, and while this fixes this particular program, it introduces a myriad of test failures elsewhere:

Unexpected results from:
TEST="Dep05 T13035 T14515 T9858a syn-perf2 tc160 tc238"

These can be categorized into the following categories:

  • Unexpected failures (T14515, tc160, T9858a)

This is tricky. Consider the following minimized example:

{-# LANGUAGE RankNTypes #-}
module A where

type Foo = forall a. a -> a
module B where

import A

foo :: Foo -> a -> a
foo f x = f x

Currently, GHC HEAD accepts B. If we apply your suggested change, however, it is rejected:

$ ~/Software/ghc/inplace/bin/ghc-stage2 B.hs
[1 of 2] Compiling A                ( A.hs, A.o )
[2 of 2] Compiling B                ( B.hs, B.o )

B.hs:5:8: error:
    • Illegal polymorphic type: forall a1. a1 -> a1
      Perhaps you intended to use RankNTypes or Rank2Types
    • In the expansion of type synonym ‘Foo’
      In the type signature: foo :: Foo -> a -> a
  |
5 | foo :: Foo -> a -> a
  |        ^^^^^^^^^^^^^

Is this desirable? FWIW, GHC 8.6 also rejects B—it's only the current GHC HEAD that accepts it.

  • Timeouts (T13035, tc238, syn-perf2)

It appears that having to fully expand every type synonym for validity-checking purposes imposes quite a bit of runtime cost.

  • Error message wibbles (Dep05)

This happens simply because the more aggressive validity checking happens earlier now:

  • safeHaskell/unsafeLibs/Dep05.run/Dep05.

    diff -uw "safeHaskell/unsafeLibs/Dep05.run/Dep05.stderr.normalised" "safeHaskell/unsafeLibs/Dep05.run/Dep05.comp.stderr.normalised"
    old new  
    11
    2 Dep05.hs:5:1:
    3     GHC.Arr: Can't be safely imported! The module itself isn't safe.
     2Dep05.hs:9:1:
     3     Illegal unboxed tuple type as function argument:
     4      (# GHC.Prim.State# s, a #)
     5      Perhaps you intended to use UnboxedTuples
     6     In the expansion of type synonym ‘GHC.ST.STRep’
     7      When checking the inferred type
     8        bad2 :: forall s e a.
     9                GHC.Prim.MutableArray# s e
     10                -> (Int, e) -> GHC.ST.STRep s a -> GHC.ST.STRep s a
     11
     12Dep05.hs:11:1:
     13     Illegal unboxed tuple type as function argument:
     14      (# GHC.Prim.State# s, Array i e #)
     15      Perhaps you intended to use UnboxedTuples
     16     In the expansion of type synonym ‘GHC.ST.STRep’
     17      When checking the inferred type
     18        bad3 :: forall i s e.
     19                i
     20                -> i
     21                -> Int
     22                -> GHC.Prim.MutableArray# s e
     23                -> GHC.ST.STRep s (Array i e)

This isn't too big of a deal, since we can suppress the new error message by enabling UnboxedTuples.

The synIsTau field of a SynonymTyCon might allow us to short-circuit the common case where the RHS is totally vanilla. (To do so we'd need to ensure that synIsTau is false if there is a => in the RHS, not just a forall.)

That would work for this particular example, although there will likely be other validity checks that can't take advantage of this synIsTau shortcut. In fact, the original place I discovered this bug was in the context of a WIP patch I have which adds visible dependent quantification (i.e., this GHC proposal). I discovered that GHC rejects this (since we can't yet have visible dependent quantification in the type of a term):

f :: forall k -> k -> Bool
f = undefined

But does accept this:

type Foo = forall k -> k -> Bool

f :: Foo
f = undefined

The reason this happens is for the same reason as the original program in this ticket, so it would be nice if we could come up with a fix that covers both programs.

comment:4 Changed 10 months ago by simonpj

T14515 and friends. I think it's reasonable to reject. Type synonyms are not proper abstractions; they are more like macros. The current behaviour:

  • Triggers unexpected new errors when you switch on LiberalTypeSynonyms.
  • Ditto if you manually expand a synonym, which should be innocuous.

Timeouts. Look at tc238. I thought at first that we were simply making an exponentially large type, as we easily could do:

type T1 = Int -> Int   -- Size = N
type T2 = T1 -> T1     -- Size = 2N
type T3 = T2 -> T2     -- Size = 4N
..

For such programs, I think it'd be fine to time out; we'd time out when using such a large synonym anyway.

But that is NOT what is happening here. For tc238 we have

data T i r c = K (c i) (r c)

type TIACons2  t x = T t (T t x)
type TIACons3  t x = TIACons2 t (TIACons1 t x)
type TIACons4  t x = TIACons2 t (TIACons2 t x)
type TIACons7  t x = TIACons4 t (TIACons3 t x)
type TIACons8  t x = TIACons4 t (TIACons4 t x)

So TIACons2 has two occurrences of T; TIACons3 has three, TIACons4 has four; and so on. The number in the name indicates the number of occurrences of T. Big but not exponential.

The problem comes because at each synonym we check validity with and without expansion. So if we have

type S = ...
f :: S (S (S (S (S (S ....(S Int)...))))

we'll typecheck the outer S application with and without expansion; and in each of those checks we'll check the next S application with and without... result exponential! This goes right back to Trac #323, 14 years ago.

What to do? In general, we can't check both with and without expansion. So we could do one of these:

  1. Always expand. That is simple and sound, but I suppose that it might occasionally yield a worse error message.
  1. Always expand; but if you get an error message, then try without expansion to see if you also get an error; in the latter case report the latter error message not the former.
  1. Within the validity checker have a 3-way flag: Expand, NoExpand, Both. For Liberal start with Expand; for non-Liberal start with Both.

Now at a synonym, in the Both case, switch to NoExpand when checking the non-expanded version, and to Both when checking the expanded version.

I think (1) seems like a simpler starting point.


I agree about synIsTau.

comment:5 Changed 10 months ago by goldfire

The problem in this code

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where

type Foo b = Eq b => b

f :: forall b (a :: Foo b). Int
f = 42

is the definition of Foo, not the usage of it. As comment:3 illustrates and comment:4 elaborates, we don't really want to check the expansion of a type synonym in this way. (Hold off on considering LiberalTypeSynonyms for now.) Even with the rather transparent interpretation of type synonyms in GHC, I think they should offer some level of abstraction (in contrast to the position in comment:4): it seems that allowing type synonyms at least to hide what extensions are enabled is sensible.

What about LiberalTypeSynonyms? I don't know. But let's see if we can agree on conservative synonyms first, and then we'll move to liberal ones.

comment:6 Changed 10 months ago by simonpj

But there is nothing fundamentally wrong with Foo. You might write

f :: Foo Int

which means the same as

f :: Eq Int => Int

which is a perfectly legal type.

checkValidType checks for reasons a type might be invalid other than its kind. Are you sure you want type synonyms to hide all the things we check thereby?

TL;DR: I'm suggesting that if it's valid, it should be valid after expanding synonyms. You are suggesting that they should offer some level of abstraction. I'm unconvinced. Exactly what level of abstraction?

comment:7 Changed 10 months ago by goldfire

Silly me. I looked quickly and assumed that the problem was the lack of a -XQuantifiedConstraints. This is clearly wrong.

Bah. I guess I take back my comment:5 then, as I can't see any better way out of this mess other than to implement kind-level constraints, which, in turn, requires dependent types.

comment:8 Changed 10 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:9 Changed 9 months ago by Iceland_jack

Cc: Iceland_jack added

comment:10 Changed 9 months ago by RyanGlScott

Blocking: 16140 added

comment:11 Changed 9 months ago by RyanGlScott

For the sake of gathering more examples, this also manifests when checking unboxed tuples. For instance, GHC compiles B.hs below successfully, even though it shouldn't (since the UnboxedTuples extension isn't enabled in B):

{-# LANGUAGE UnboxedTuples #-}
module A where

type Foo = (# #)
-- B.hs
module B where

import A

type Bar = Foo

On the other hand, in C.hs below:

-- C.hs
{-# LANGUAGE TemplateHaskell #-}
module C where

import Language.Haskell.TH (conT, unboxedTupleTypeName)

type Baz = $(conT (unboxedTupleTypeName 0))

GHC correctly rejects this, since there's no intermediate type synonym:

C.hs:7:1: error:
    • Illegal unboxed tuple type as function argument: (# #)
      Perhaps you intended to use UnboxedTuples
    • In the type synonym declaration for ‘Baz’
  |
7 | type Baz = $(conT (unboxedTupleTypeName 0))
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This also affects RankNTypes, since B.hs is erroneously accepted:

-- A.hs
{-# LANGUAGE RankNTypes #-}
module A where

type Foo = forall a. a
-- B.hs
module B where

import A

f :: Foo -> b -> b
f g x = g x

comment:12 Changed 9 months ago by RyanGlScott

It turns out that option (1) from comment:4 is just plain infeasible. If you implement it, then several test cases that should fail suddenly pass. tcfail129 is one example:

module ShouldFail where

data T = T

-- This was erroneously accepted
type Foo a = String -> Maybe a
type Bar m = m Int
blah = undefined :: Bar Foo


type Foo1 a = Maybe a
type Bar1 m = m Int
blah1 = undefined :: Bar1 Foo1

This should fail due to the unsaturated use of Foo/Foo1, but if we always expand, then we'll never catch that!

comment:13 Changed 9 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/112
Status: newpatch

Option (3) from comment:4 ended up being just the ticket to fixing this bug. See https://gitlab.haskell.org/ghc/ghc/merge_requests/112.

comment:14 Changed 9 months ago by RyanGlScott

Status: patchupstream

As noted in https://gitlab.haskell.org/ghc/ghc/merge_requests/112#note_2409, the MR I linked to above is failing to validate due to a sneaky use of impredicativity in Cabal that went unnoticed until this patch revealed it. I've opened a Cabal issue upstream here.

comment:15 Changed 9 months ago by simonpj

As noted in my comment on the MR, I don't think this is Cabal's fault.

I took a quick look but I can't see immediately why that is happening.

comment:17 Changed 9 months ago by RyanGlScott

Blocking: 16140 removed
Milestone: 8.10.18.8.1
Resolution: fixed
Status: upstreamclosed
Test Case: typecheck/should_fail/T16059{a,c,d,e}

comment:18 Changed 9 months ago by Ryan Scott <ryan.gl.scott@…>

In 9dc56b6/ghc:

Control validity-checking of type synonym applications more carefully

Trac #16059 shows that when validity checking applications of type
synonyms, GHC sometimes wasn't checking the expanded type enough.
We must be careful, however, since checking both the expanded type as
well as the arguments to the type synonym can lead to exponential
blowup (see https://ghc.haskell.org/trac/ghc/ticket/16059#comment:4).
Nor can we omit checking either the expanded type or the argument for
correctness reasons.

The solution here is to introduce a new `ExpandMode` data type that
is plumbed through all of the type-validity-checking functions in
`TcValidity`. `ExpandMode` dictates whether we only check the
expanded type (`Expand`), only check the arguments (`NoExpand), or
both (`Both`). Importantly, if we check `Both` in the function for
validity checking type synonym applications, then we switch to
`NoExpand` when checking the arguments so as to avoid exponential
blowup. See `Note [Correctness and performance of type synonym validity
checking]` for the full story.
Note: See TracTickets for help on using tickets.