Strange constraint error that disappears when adding another top-level declaration
Consider this program:
```hs
{-# 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.
<details><summary>Trac metadata</summary>
| 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 | |
</details>
<!-- {"blocked_by":[],"summary":"Strange constraint error that disappears when adding another top-level declaration","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this program:\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}\r\nmodule CURepro where\r\n\r\nimport Data.Kind\r\n\r\ndata NP (f :: Type -> Type) (xs :: [Type])\r\n\r\ntype family Curry (f :: Type -> Type) (xs :: [Type]) (r :: Type) (a :: Type) :: Constraint where\r\n Curry f xs r (f x -> a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)\r\n Curry f xs r a = (xs ~ '[], r ~ a)\r\n\r\ntype family Tail (a :: [Type]) :: [Type] where\r\n Tail (_ : xs) = xs\r\n\r\nuncurry_NP :: (Curry f xs r a) => (NP f xs -> r) -> a\r\nuncurry_NP = undefined\r\n\r\nfun_NP :: NP Id xs -> ()\r\nfun_NP = undefined\r\n\r\nnewtype Id a = MkId a\r\n\r\n-- test1 :: ()\r\n-- test1 = uncurry_NP fun_NP (MkId 5)\r\n\r\ntest2 :: ()\r\ntest2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n}}}\r\n\r\nWith GHC 8.6.1 (and also 8.4.3), this produces the following error message:\r\n{{{\r\nCURepro.hs:27:9: error:\r\n • Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’\r\n arising from a use of ‘uncurry_NP’\r\n The type variable ‘t0’ is ambiguous\r\n • In the expression:\r\n uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n In an equation for ‘test2’:\r\n test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n |\r\n27 | test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nHowever, uncommenting the definition of `test1` makes the whole program check without error!\r\n\r\nI think both versions of the program should be accepted.\r\n\r\nI'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.","type_of_failure":"OtherFailure","blocking":[]} -->
issue