#8705: Type inference regression with local dictionaries --------------------------------------------+------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: high | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by goldfire): Here is a version without the `singletons` dependency: {{{ {-# LANGUAGE TypeOperators, DataKinds, PolyKinds, MultiParamTypeClasses, GADTs, ConstraintKinds, TypeFamilies #-} module Bug where data family Sing (a :: k) data Proxy a = Proxy data instance Sing (a :: Maybe k) where SJust :: Sing h -> Sing (Just h) data Dict c where Dict :: c => Dict c -- A less-than-or-equal relation among naturals class a :<=: b sLeq :: Sing n -> Sing n2 -> Dict (n :<=: n2) sLeq = undefined insert_ascending :: (lst ~ Just n1) => Proxy n1 -> Sing n -> Sing lst -> Dict (n :<=: n1) insert_ascending _ n (SJust h) = case sLeq n h of Dict -> Dict }}} Interestingly, when I tried getting rid of the data family, the code started compiling. Perhaps there's a problem with normalisation somewhere? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8705#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler