[GHC] #13705: Failure of improvement for type-family dependencies
#13705: Failure of improvement for type-family dependencies -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider {{{ {-# LANGUAGE TypeFamilyDependencies #-} data D x type family F t = s | s -> t type instance F (D t) = D (F t) f :: F s -> () f _ = () g :: D (F t) -> () g x = f x }}} which was presented in [https://mail.haskell.org/pipermail/haskell- cafe/2016-October/125375.html this email] from Clinton Mead. It yields {{{ Tx.hs:14:9: error: • Couldn't match expected type ‘F s0’ with actual type ‘D (F t)’ The type variable ‘s0’ is ambiguous }}} But it should work fine -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13705 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13705: Failure of improvement for type-family dependencies -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This program shows up a bug in the pure unifier in `Unify.hs`. Look at {{{ unify_ty ty1 (TyVarTy tv2) kco = do { unif <- amIUnifying ; if unif then umSwapRn $ uVar tv2 ty1 (mkSymCo kco) else surelyApart } -- non-tv on left; tv on right: can't match. }}} If we are matching {{{ F a ~ b }}} where `F` is a type function, we want to ''succeed'', not return `SurelyApart`, because in Algorithm U/M from the paper, type function applications are treated like wildcards. And indeed a later equation deals with that case {{{ unify_ty ty1 _ _ | Just (tc1, _) <- splitTyConApp_maybe ty1 , not (isGenerativeTyCon tc1 Nominal) = maybeApart }}} It's just that the type-variable case was too eager. Easy to fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13705#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13705: Failure of improvement for type-family dependencies -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): For the record, I agree with comment:1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13705#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13705: Failure of improvement for type-family dependencies
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#13705: Failure of improvement for type-family dependencies -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The reason this hasn't caused chaos sooner is that the pure unifier should never really see type functions. The only place it does, I believe, is in checking injectivity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13705#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13705: Failure of improvement for type-family dependencies -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T13705 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => indexed-types/should_compile/T13705 Comment: Might be worth merging, but definitely not essential. I ended up refactoring the unifer to make the environment an explicit parameter, so that it's easier to use in guards. So the patch is bigger than it "needs" to be. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13705#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13705: Failure of improvement for type-family dependencies -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T13705 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed * milestone: => 8.2.1 Comment: Merged in aa39137316fcbb555bcb676cb2f89002d97d3e3c. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13705#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC