Constraint resolution vs. type family resolution vs. TypeErrors

Via http://stackoverflow.com/q/37769351/477476, given the following setup:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-}

import Data.Proxy
import GHC.TypeLits

type family TEq a b where
    TEq a a = a
    TEq a b = TypeError (Text "TEq error")

type family F a where
    F () = ()
    F (a, b) = TEq (F a) (F b)
    F a = TypeError (Text "Unsupported type: " :<>: ShowType a)

and the following usages of F and TEq:

class (repr ~ F a) => C repr a

foo :: (C (F a) a) => proxy a -> ()
foo _ = ()

main :: IO ()
main = print $ foo (Proxy :: Proxy (Int, ()))

This results in

    * No instance for (C (TEq (TypeError ...) ()) (Int, ()))
        arising from a use of `foo'
    * In the second argument of `($)', namely
        `foo (Proxy :: Proxy (Int, ()))'
      In the expression: print $ foo (Proxy :: Proxy (Int, ()))
      In an equation for `main':
          main = print $ foo (Proxy :: Proxy (Int, ()))

but it would be preferable to bail out earlier when F Int is resolved to TypeError ... instead of propagating that all the way to the C constraint.

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture