[GHC] #13295: Failure to resolve type parameter determined by type family

[GHC]

#13295: Failure to resolve type parameter determined by type family
-------------------------------------+-------------------------------------
           Reporter:  alexvieth      |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}

 import Data.Proxy

 -- Defined to get the type forall x . 'D x
 data D where
   D :: a -> D

 type family F t :: D

 -- Will try to create values of this type through the type family
 -- F, i.e. G (F t)
 data G (d :: D) where
   G :: G ('D x)

 -- This is rejected because the type variable x in 'D x is ambiguous.
 -- But is it really? If there's an instance of F t then x is determined.
 introG :: Proxy t -> G (F t)
 introG _ = G

 -- introG is well-typed if we add an equality constraint.
 -- Can GHC not figure this out without our help?
 introG' :: forall t x . ( F t ~ 'D x ) => Proxy t -> G (F t)
 introG' _ = G
 }}}

 Here's the type error:

 {{{
     • Couldn't match type ‘F t’ with ‘'D x0’
       Expected type: G (F t)
         Actual type: G ('D x0)
       The type variable ‘x0’ is ambiguous
     • In the expression: G
       In an equation for ‘introG’: introG _ = G
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13295>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler