[GHC] #12237: Constraint resolution vs. type family resolution vs. TypeErrors

27 Jun 2016

      #12237: Constraint resolution vs. type family resolution vs. TypeErrors
-------------------------------------+-------------------------------------
           Reporter:  cactus         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  CustomTypeErrors                   |
       Architecture:                 |   Type of failure:  Other
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Via http://stackoverflow.com/q/37769351/477476, given the following setup:

 {{{#!hs
 {-# 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`:

 {{{#!hs
 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12237
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler