Opened 3 years ago

Closed 2 years ago

#12237 closed feature request (duplicate)

Constraint resolution vs. type family resolution vs. TypeErrors

Reported by: cactus Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: CustomTypeErrors Cc: crockeea, diatchki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Other Test Case:
Blocked By: Blocking:
Related Tickets: #11990 Differential Rev(s):
Wiki Page:

Description

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.

Change History (3)

comment:1 Changed 3 years ago by crockeea

Cc: crockeea added

comment:2 Changed 3 years ago by thomie

Cc: diatchki added

This seems fixed in GHC HEAD (c88f31a08943764217b69adb1085ba423c9bcf91, 8.1.20160610), perhaps as a result of #11990.

Test.hs:23:16: error:
    • Unsupported type: Int
    • 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, ()))

comment:3 Changed 2 years ago by RyanGlScott

Resolution: duplicate
Status: newclosed

Indeed, this is fixed in 8.0.2. This test case is sufficiently similar to the one in #11990 that I'll close this as a duplicate.

Note: See TracTickets for help on using tickets.