Opened 4 months ago

Last modified 2 months ago

#14038 new bug

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

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.4.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:
Blocked By: #14119 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 (14)

comment:1 Changed 4 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 4 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 4 months ago by RyanGlScott

Cc: goldfire added

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

comment:4 Changed 4 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 4 months ago by goldfire

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

comment:6 Changed 3 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 3 months ago by goldfire

Blocked By: 14119 added

comment:8 Changed 3 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 3 months ago by simonpj

#13910 may be another manifestation of this bug.

comment:10 Changed 3 months ago by simonpj

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

comment:11 Changed 3 months ago by goldfire

Do you have any input re comment:6?

comment:12 Changed 3 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 3 months ago by simonpj

#13938 may be another manifestation.

It'd be good to nail this one.

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

In 3b68687/ghc:

Test #14038 in dependent/should_compile/T14038
Note: See TracTickets for help on using tickets.