Deep subsumption does not instantiate in cases where it should
See also:
* #12563
There are many situations in which one would expect deep subsumption to allow a program to be accepted, yet it doesn't.
Here follows a collection of examples. I've used partial type signatures for simplicity, but the same errors can be triggered without it. Examples `ex1'`, `ex2'`, `ex3` and `ex3'` are all incorrectly rejected.
```hs
{-# LANGUAGE DeepSubsumption #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module T26225 where
-- Recall: ty1 is a subtype of ty2, written ty1 ⊑ ty2,
-- if we can use ty1 wherever ty2 is expected.
-- Example: ∀ a. a -> a ⊑ Int -> Int, meaning that we can pass
-- the identity function where one is expecting a function of type Int -> Int.
-- Int -> (∀ a. a -> a) ⊑ α[tau]
-- Accepted by GHC.
ex0 :: ()
ex0 =
let
f :: Int -> (∀ a. a -> a)
f _ = id
g :: _α -> ()
g _ = ()
in g f
-- ((∀ a. a->a) -> Int) -> Bool ⊑ α[tau]
-- Rejected by GHC up to and including 9.14.
ex1' :: ()
ex1' =
let
f :: ((∀ a. a -> a) -> Int) -> Bool
f _ = False
g :: _α -> ()
g _ = ()
in g f
-- Couldn't match expected type ‘α’ with actual type ‘((∀ a. a -> a) -> Int) -> Bool’
-- ((∀ a. a->a) -> Int) -> Bool ⊑ β[tau] Bool
-- Rejected by GHC up to and including 9.14.
ex2' :: ()
ex2' =
let
f :: ((∀ a. a -> a) -> Int) -> Bool
f _ = False
g :: _β Bool -> ()
g _ = ()
in g f
-- Couldn't match expected type ‘β’ with actual type ‘(->) ((∀ a. a -> a) -> Int)’
-- ex3 :: β[tau] Bool ⊑ (∀ a. a->a) -> Bool
-- Rejected by GHC up to and including 9.14.
ex3 :: ()
ex3 =
let
f :: _β Bool
f = undefined
g :: ((∀ a. a -> a) -> Bool) -> ()
g _ = ()
in g f
-- Couldn't match expected type ‘β’ with actual type ‘(->) (∀ a. a -> a)’
-- ex3' :: F Int Bool ⊑ (∀ a. a->a) -> Bool, where F Int = (->) (Int -> Int)
-- Rejected by GHC up to and including 9.14.
ex3' :: ()
ex3' =
let
f :: F Int Bool
f _ = False
g :: ((∀ a. a -> a) -> Bool) -> ()
g _ = ()
in g f
-- • Couldn't match type: Int -> Int
-- with: ∀ a. a -> a
-- Expected: (∀ a. a -> a) -> Bool
-- Actual: F Int Bool
type family F a where { F Int = (->) (Int -> Int) }
```
issue