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 |