Opened 10 months ago

Closed 2 months ago

#14038 closed bug (fixed)

TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.3
Keywords: TypeApplications Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: dependent/should_compile/T14038
Blocked By: Blocking:
Related Tickets: #13877 Differential Rev(s):
Wiki Page:

Description

This file:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Eliminator where

import Data.Kind (Type)

data family Sing (a :: k)
data instance Sing (z :: [a]) where
  SNil  :: Sing '[]
  SCons :: Sing x -> Sing xs -> Sing (x:xs)

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@

data FunArrow = (:->) -- ^ '(->)'
              | (:~>) -- ^ '(~>)'

class FunType (arr :: FunArrow) where
  type Fun (k1 :: Type) arr (k2 :: Type) :: Type

class FunType arr => AppType (arr :: FunArrow) where
  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2

type FunApp arr = (FunType arr, AppType arr)

instance FunType (:->) where
  type Fun k1 (:->) k2 = k1 -> k2

instance AppType (:->) where
  type App k1 (:->) k2 (f :: k1 -> k2) x = f x

instance FunType (:~>) where
  type Fun k1 (:~>) k2 = k1 ~> k2

instance AppType (:~>) where
  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x

infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2

elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
            Sing l
         -> p '[]
         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
         -> p l
elimList = elimListPoly @(:->)

elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
                 Sing l
              -> p @@ '[]
              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
              -> p @@ l
elimListTyFun = elimListPoly @(:~>) @_ @p

elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
                FunApp arr
             => Sing l
             -> App [a] arr Type p '[]
             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
             -> App [a] arr Type p l
elimListPoly SNil                      pNil _     = pNil
elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)

Typechecks in GHC 8.2.1 without issue, but fails in GHC HEAD:

$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170725: http://www.haskell.org/ghc/  :? for help                      
Loaded GHCi configuration from /home/rgscott/.ghci                                        
[1 of 1] Compiling Eliminator       ( Bug.hs, interpreted )                               
                                                                                          
Bug.hs:59:12: error:                                                                      
    • Couldn't match type ‘p0’ with ‘p’                                                   
        because type variables ‘a1’, ‘p’ would escape their scope                         
      These (rigid, skolem) type variables are bound by                                   
        the type signature for:                                                           
          elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).                             
                      Sing l                                                              
                      -> p '[]                                                            
                      -> (forall (x :: a1) (xs :: [a1]).                                  
                          Sing x -> Sing xs -> p xs -> p (x : xs))                        
                      -> p l                                                              
        at Bug.hs:(54,1)-(58,15)                                                          
      Expected type: Sing l                                                               
                     -> p '[]                                                             
                     -> (forall (x :: a1) (xs :: [a1]).
                         Sing x -> Sing xs -> p xs -> p (x : xs))
                     -> p l
        Actual type: Sing l
                     -> App [a1] (':->) * p0 '[]
                     -> (forall (x :: a1) (xs :: [a1]).
                         Sing x
                         -> Sing xs
                         -> App [a1] (':->) * p0 xs
                         -> App [a1] (':->) * p0 (x : xs))
                     -> App [a1] (':->) * p0 l
    • In the expression: elimListPoly @(:->)
      In an equation for ‘elimList’: elimList = elimListPoly @(:->)
    • Relevant bindings include
        elimList :: Sing l
                    -> p '[]
                    -> (forall (x :: a1) (xs :: [a1]).
                        Sing x -> Sing xs -> p xs -> p (x : xs))
                    -> p l
          (bound at Bug.hs:59:1)
   |
59 | elimList = elimListPoly @(:->)
   |            ^^^^^^^^^^^^^^^^^^^

Bug.hs:59:12: error:
    • Couldn't match type ‘p0’ with ‘p’
        ‘p0’ is untouchable
          inside the constraints: ()
          bound by a type expected by the context:
                     forall (x :: a1) (xs :: [a1]).
                     Sing x
                     -> Sing xs
                     -> App [a1] (':->) * p0 xs
                     -> App [a1] (':->) * p0 (x : xs)
          at Bug.hs:59:12-30
      ‘p’ is a rigid type variable bound by
        the type signature for:
          elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).
                      Sing l
                      -> p '[]
                      -> (forall (x :: a1) (xs :: [a1]).
                          Sing x -> Sing xs -> p xs -> p (x : xs))
                      -> p l
        at Bug.hs:(54,1)-(58,15)
      Expected type: Sing x
                     -> Sing xs
                     -> App [a1] (':->) * p0 xs
                     -> App [a1] (':->) * p0 (x : xs)
        Actual type: Sing x -> Sing xs -> p xs -> p (x : xs)
    • In the expression: elimListPoly @(:->)
      In an equation for ‘elimList’: elimList = elimListPoly @(:->)
    • Relevant bindings include
        elimList :: Sing l
                    -> p '[]
                    -> (forall (x :: a1) (xs :: [a1]).
                        Sing x -> Sing xs -> p xs -> p (x : xs))
                    -> p l
          (bound at Bug.hs:59:1)
   |
59 | elimList = elimListPoly @(:->)
   |            ^^^^^^^^^^^^^^^^^^^

A workaround is to explicitly apply p with TypeApplications in line 59:

elimList = elimListPoly @(:->) @_ @p

Change History (16)

comment:1 Changed 10 months ago by RyanGlScott

If this bug is fixed, we should see if the program in https://ghc.haskell.org/trac/ghc/ticket/13877#comment:2 panics or not, since whether it panics or not is masked by the bug in this ticket.

comment:2 Changed 10 months ago by simonpj

Richard, in a -DDEBUG compiler this falls over with

Following filled tyvar a_a225[tau:2] = a_a220[sk:2]
Unfilled tyvar a_a220[sk:2]
flatten/appty
  (p0_a226[tau:2] |> T14038.D:R:Funk1:->k2[0] <k1>_N <k2>_N)
  '[]
  p0_a226[tau:2]
  '[]
  nominal
  nominal
flatten } p0_a226[tau:2] '[]
New coercion hole: a23h
Emitting new coercion holeghc-stage1: panic! (the 'impossible' happened)
  (GHC version 8.3.20170726 for x86_64-unknown-linux):
	piResultTy
  Fun [a_a220[sk:2]] (':->) *
  '[]
  Call stack:
      ?callStack, called at compiler/utils/Util.hs:1394:50 in ghc:Util
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

I think what is happening is that we start with (p0_a226 |> co) '[], where p0_a226 :: Fun [a_a220[sk:2]] (':->) *, and co casts it to a function type. But then flattening throws away the cats, apparently, and we try to form (mkAppTy p0_a226 '[]), which is simply ill-kinded.

I have (again) lost track of what is supposed to happen here.

comment:3 Changed 10 months ago by RyanGlScott

Cc: goldfire added

Commit 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 (Improve error messages around kind mismatches.) caused this regression.

comment:4 Changed 10 months ago by Simon Peyton Jones <simonpj@…>

In ad0037e/ghc:

Add DebugCallStack to piResultTy

This was provoked by an ASSERT failure when debugging #14038,
but it's a godo idea anyway.

comment:5 Changed 10 months ago by goldfire

This may be fixed by #12919, which I plan to tackle in the next few days.

comment:6 Changed 10 months ago by goldfire

My local fix for #12919 does fix this. But then a deeper bug lurks.

The problem is that the App instance for (:~>) gets type-checked with a coercion in its patterns. Of course, the type-family matcher can't deal with a coercion pattern -- what would such a thing mean anyway? So it does something stupid. In this case, the stupid thing is that the match result contains an unbound variable, but it could conceivably do a different stupid thing tomorrow.

The solution, of course, is to make sure that type patterns never contain coercions. I've been meaning to do this for a long time, regardless. (I don't think there's a ticket to track the idea, though.) I see two possible approaches:

  1. Parameterize the code in TcHsType to know whether it's reading a pattern or a normal type, and don't make coercions in patterns.
  1. Have TcHsType proceed normally, but rip the coercions out after-the-fact.

What to do in the spots where the coercions used to be? Insert bare coercion variables, which can then be solved for. Some perhaps-outdated thoughts on this are here, but those notes were meant more for myself than anyone else.

While we're thinking about this, another question I've pondered for a while: should type patterns be a separate datatype in GHC than Type? For example, a type pattern never has a type function nor a forall. It won't have meaningful CastTys or CoercionTys either. With this change, the pure unifier could perhaps be simplified.

In any case, more thought is necessary.

comment:7 Changed 9 months ago by goldfire

Blocked By: 14119 added

comment:8 Changed 9 months ago by goldfire

I've made a new ticket to discuss how to deal with type patterns at #14119, which this ticket is blocked by.

comment:9 Changed 9 months ago by simonpj

#13910 may be another manifestation of this bug.

comment:10 Changed 9 months ago by simonpj

I think we won't pursue #14119, so this ticket is live again.

comment:11 Changed 9 months ago by goldfire

Do you have any input re comment:6?

comment:12 Changed 9 months ago by simonpj

comment:6 says:

The problem is that the App instance for (:~>) gets type-checked with a coercion in its patterns

Can you boil this out into a simple case? I'm lost.

Have TcHsType proceed normally, but rip the coercions out after-the-fact.

That's what happens in Rules. See DsBinds.decomposeRuleLhs.

comment:13 Changed 9 months ago by simonpj

#13938 may be another manifestation.

It'd be good to nail this one.

comment:14 Changed 8 months ago by Ben Gamari <ben@…>

In 3b68687/ghc:

Test #14038 in dependent/should_compile/T14038

comment:15 Changed 2 months ago by Richard Eisenberg <rae@…>

In e3dbb44f/ghc:

Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.

comment:16 Changed 2 months ago by RyanGlScott

Blocked By: 14119 removed
Milestone: 8.4.18.6.1
Resolution: fixed
Status: newclosed
Test Case: dependent/should_compile/T14038
Note: See TracTickets for help on using tickets.