#8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!) --------------------------------------------+------------------------------ Reporter: carter | Owner: Type: feature request | Status: new Priority: normal | Milestone: 7.10.1 Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: #4259 --------------------------------------------+------------------------------ Comment (by goldfire): If you just want a way to check things, please see [https://gist.github.com/goldfirere/6902431 here]. The key step is that you do in fact have to write proofs! These proofs may, sadly, have runtime significance. But, from the optimization results in the "Deferred type errors" [http://research.microsoft.com/en- us/um/people/simonpj/papers/ext-f/icfp12.pdf paper] lead me to wonder if these runtime traces are optimized away. (I haven't checked -- doing so is beyond the scope of my morning Haskell stretches.) I did check, though, that the inliner will remove calls to `gcoerce` and make `go` properly tail-recursive (ignoring the type-cast, which I know is removed at runtime). Thanks for posting this! It's made me realize that `gcoerce` from that example should probably be in the Data.Type.Equality module anyway. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8423#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler