Strange constraint error that disappears when adding another top-level declaration

Consider this program:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
module CURepro where

import Data.Kind

data NP (f :: Type -> Type) (xs :: [Type])

type family Curry (f :: Type -> Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where
  Curry f xs r (f x -> a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
  Curry f xs r a          = (xs ~ '[], r ~ a)

type family Tail (a :: [Type]) :: [Type] where
  Tail (_ : xs) = xs

uncurry_NP :: (Curry f xs r a) => (NP f xs -> r) -> a
uncurry_NP = undefined

fun_NP :: NP Id xs -> ()
fun_NP = undefined

newtype Id a = MkId a

-- test1 :: ()
-- test1 = uncurry_NP fun_NP (MkId 5)

test2 :: ()
test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)

With GHC 8.6.1 (and also 8.4.3), this produces the following error message:

CURepro.hs:27:9: error:
    • Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’
        arising from a use of ‘uncurry_NP’
      The type variable ‘t0’ is ambiguous
    • In the expression:
        uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
      In an equation for ‘test2’:
          test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
   |
27 | test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

However, uncommenting the definition of test1 makes the whole program check without error!

I think both versions of the program should be accepted.

I've tried to extract this from a much larger failing example, but did not manage to make it any smaller than this. In particular, the fact that NP is parameterised over a type constructor f seems to be somehow essential to trigger this.

Trac metadata

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