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

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

Trac metadata

Trac field	Value
Version	8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture