TypeError reported too eagerly

Consider the following example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

data DUMMY

type family If c t e where
   If True t e  = t
   If False t e = e


type family F (n :: Nat) where
   --F n = If (n <=? 8) Int (TypeError (Text "ERROR"))
   F n = If (n <=? 8) Int DUMMY

test :: (F n ~ Word) => Proxy n -> Int
test _ = 2

test2 :: Proxy (n :: Nat) -> Int
test2 p = test p

main :: IO ()
main = do
   print (test2 (Proxy :: Proxy 5))

The type error is useful:

Bug.hs:26:11: error:
    • Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’
        arising from a use of ‘test’
    • In the expression: test p
      In an equation for ‘test2’: test2 p = test p
    • Relevant bindings include
        p :: Proxy n (bound at Bug.hs:26:7)
        test2 :: Proxy n -> Int (bound at Bug.hs:26:1)
   |
26 | test2 p = test p
   |           ^^^^^^

Now if we use the commented implementation of F (using TypeError), with GHC 8.2.2 and 8.0.2 we get:

Bug.hs:26:11: error:
    • ERROR
    • In the expression: test p
      In an equation for ‘test2’: test2 p = test p
   |
26 | test2 p = test p
   |           ^^^^^^

While with GHC 8.0.1 we get:

/home/hsyl20/tmp/Bug.hs:29:11: error:
    • Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’
                     with ‘Word’
        arising from a use of ‘test’
    • In the expression: test p
      In an equation for ‘test2’: test2 p = test p

1. Could we restore the behavior of GHC 8.0.1?

2. In my real code, when I use DUMMY I get:

    • Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’
      Expected type: Word
        Actual type: F n

If we could get the same report (mentioning the "Actual type") when we use TypeError that would be great.

Trac metadata

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