#14570: Untouchable error arises from type equality, but not equivalent program with fundeps -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Consider {{{ {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, GADTs, FunctionalDependencies #-} class C k a | k -> a data T a where MkT :: (a ~ Bool) => a -> T a data S a where MkS :: (C Bool a) => a -> S a f1 (MkT x) = x f2 (MkS x) = x }}} Here, `f2` typechecks fine, yielding `f2 :: S a -> a`. But `f1` is rejected with an untouchable-tyvar error. But, as in your emample, one has a fundep and the other has a type equality. Reason: fundeps affect only type inference, causing more unifications to happen. They do not carry evidence, and are not reflected in GHC's internal language System FC. Schrijvers et al have [https://people.cs.kuleuven.be/~tom.schrijvers/portfolio/haskell2017a.html a paper about this in at HS'17]. I haven't unpicked your example precisely but I wanted to give you a simple case in which fundeps and type equalities behave differently, by design. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14570#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler