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

[GHC]

#14038: TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the
constraints: ()
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.3
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This file:

 {{{#!hs
 {-# 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:

 {{{#!hs
 elimList = elimListPoly @(:->) @_ @p
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14038>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler