[GHC] #12237: Constraint resolution vs. type family resolution vs. TypeErrors
GHC
ghc-devs at haskell.org
Tue Jun 28 02:43:44 UTC 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
More information about the ghc-tickets
mailing list