Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC

Commits:

9 changed files:

Changes:

  • compiler/GHC/Core/TyCo/Compare.hs
    ... ... @@ -229,6 +229,8 @@ tcEqTyConApps tc1 args1 tc2 args2
    229 229 
       = tc1 == tc2 && tcEqTyConAppArgs args1 args2
    230 230
    231 231 
     tcEqTyConAppArgs :: [Type] -> [Type] -> Bool
    232 
    +-- Args do not have to have equal length;
    233 
    +-- we discard the excess of the longer one
    232 234 
     tcEqTyConAppArgs args1 args2
    233 235 
       = and (zipWith tcEqTypeNoKindCheck args1 args2)
    234 236 
         -- No kind check necessary: if both arguments are well typed, then

  • compiler/GHC/Core/Unify.hs
    ... ... @@ -245,16 +245,21 @@ give up on), but for /substitutivity/. If we have (F x x), we can see that (F x
    245 245 
     can reduce to Double. So, it had better be the case that (F blah blah) can
    246 246 
     reduce to Double, no matter what (blah) is!
    247 247
    248 
    -To achieve this, `go_fam` in `uVarOrFam` does this;
    248 
    +To achieve this, `go` in `uVarOrFam` does this;
    249 
    +
    250 
    +* We maintain /two/ substitutions, not just one:
    251 
    +     * um_tv_env: the regular substitution, mapping TyVar :-> Type
    252 
    +     * um_fam_env: maps (TyCon,[Type]) :-> Type, where the LHS is a type-fam application
    253 
    +  In effect, these constitute one substitution mapping
    254 
    +     CanEqLHS :-> Types
    249 255
    250 256 
     * When we attempt to unify (G Float) ~ Int, we return MaybeApart..
    251 
    -  but we /also/ extend a "family substitution" [G Float :-> Int],
    252 
    -  in `um_fam_env`, alongside the regular [tyvar :-> type] substitution in
    253 
    -  `um_tv_env`.  See the `BindMe` case of `go_fam` in `uVarOrFam`.
    257 
    +  but we /also/ add a "family substitution" [G Float :-> Int],
    258 
    +  to `um_fam_env`. See the `BindMe` case of `go` in `uVarOrFam`.
    254 259
    255 260 
     * When we later encounter (G Float) ~ Bool, we apply the family substitution,
    256 261 
       very much as we apply the conventional [tyvar :-> type] substitution
    257 
    -  when we encounter a type variable.  See the `lookupFamEnv` in `go_fam` in
    262 
    +  when we encounter a type variable.  See the `lookupFamEnv` in `go` in
    258 263 
       `uVarOrFam`.
    259 264
    260 265 
       So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart.  Bingo.
    ... ... @@ -329,7 +334,7 @@ Wrinkles
    329 334 
        alternative path.  So `noMatchableGivenDicts` must return False;
    330 335 
        so `mightMatchLater` must return False; so when um_bind_fam_fun returns
    331 336 
        `DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`.  See
    332 
    -   `go_fam` in `uVarOrFam`
    337 
    +   `go` in `uVarOrFam`
    333 338
    334 339 
     (ATF6) When /matching/ can we ever have a type-family application on the LHS, in
    335 340 
        the template?  You might think not, because type-class-instance and
    ... ... @@ -426,6 +431,9 @@ Wrinkles
    426 431 
     (ATF12) There is a horrid exception for the injectivity check. See (UR1) in
    427 432 
       in Note [Specification of unification].
    428 433
    434 
    +(ATF13) We have to be careful about the occurs check.
    435 
    +  See Note [The occurs check in the Core unifier]
    436 
    +
    429 437 
     SIDE NOTE.  The paper "Closed type families with overlapping equations"
    430 438 
     http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
    431 439 
     tries to achieve the same effect with a standard yes/no unifier, by "flattening"
    ... ... @@ -449,6 +457,49 @@ and all is lost. But with the current algorithm we have that
    449 457 
         a a   ~    (Var A) (Var B)
    450 458 
     is SurelyApart, so the first equation definitely doesn't match and we can try the
    451 459 
     second, which does.  END OF SIDE NOTE.
    460 
    +
    461 
    +Note [Shortcomings of the apartness test]
    462 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    463 
    +Note [Apartness and type families] is very clever.
    464 
    +
    465 
    +But it still has shortcomings (#26358).  Consider unifying
    466 
    +    [F a, F Int, Int]  ~  [Bool, Char, a]
    467 
    +Working left to right you might think we would build the mapping
    468 
    +  F a   :-> Bool
    469 
    +  F Int :-> Char
    470 
    +Now we discover that `a` unifies with `Int`. So really these two lists are Apart
    471 
    +because F Int can't be both Bool and Char.
    472 
    +
    473 
    +Just the same applies when adding a type-family binding to um_fam_env:
    474 
    +  [F (G Float), F Int, G Float] ~ [Bool, Char, Iont]
    475 
    +Again these are Apart, because (G Float = Int),
    476 
    +and (F Int) can't be both Bool and Char
    477 
    +
    478 
    +But achieving this is very tricky! Perhaps whenever we unify a type variable,
    479 
    +or a type family, we should run it over the domain and (maybe range) of the
    480 
    +type-family mapping too?  Sigh.
    481 
    +
    482 
    +For now we make no such attempt.
    483 
    +* The um_fam_env has only /un-substituted/ types.
    484 
    +* We look up only /un-substituted/ types in um_fam_env
    485 
    +
    486 
    +This may make us say MaybeApart when we could say SurelyApart, but it has no
    487 
    +effect on the correctness of unification: if we return Unifiable, it really is
    488 
    +Unifiable.
    489 
    +
    490 
    +This is all quite subtle. suppose we have:
    491 
    +    um_tv_env:   c :-> b
    492 
    +    um_fam_env   F b :-> a
    493 
    +and we are trying to add a :-> F c. We will call lookupFamEnv on (F, [c]), which will
    494 
    +fail because b and c are not equal. So we go ahead and add a :-> F c as a new tyvar eq,
    495 
    +getting:
    496 
    +    um_tv_env:   a :-> F c, c :-> b
    497 
    +    um_fam_env   F b :-> a
    498 
    +
    499 
    +Does that loop, like this:
    500 
    +   a --> F c --> F b --> a?
    501 
    +No, because we do not substitute (F c) to (F b) and then look up in um_fam_env;
    502 
    +we look up only un-substituted types.
    452 503 
     -}
    453 504
    454 505 
     {- *********************************************************************
    ... ... @@ -1767,6 +1818,11 @@ uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM ()
    1767 1818 
     -- Why saturated?  See (ATF4) in Note [Apartness and type families]
    1768 1819 
     uVarOrFam env ty1 ty2 kco
    1769 1820 
       = do { substs <- getSubstEnvs
    1821 
    +--       ; pprTrace "uVarOrFam" (vcat
    1822 
    +--           [ text "ty1" <+> ppr ty1
    1823 
    +--           , text "ty2" <+> ppr ty2
    1824 
    +--           , text "tv_env" <+> ppr (um_tv_env substs)
    1825 
    +--           , text "fam_env" <+> ppr (um_fam_env substs) ]) $
    1770 1826 
            ; go NotSwapped substs ty1 ty2 kco }
    1771 1827 
       where
    1772 1828 
         -- `go` takes two bites at the cherry; if the first one fails
    ... ... @@ -1776,16 +1832,12 @@ uVarOrFam env ty1 ty2 kco
    1776 1832 
         -- E.g.    a ~ F p q
    1777 1833 
         --         Starts with: go a (F p q)
    1778 1834 
         --         if `a` not bindable, swap to: go (F p q) a
    1779 
    -    go swapped substs (TyVarLHS tv1) ty2 kco
    1780 
    -      = go_tv swapped substs tv1 ty2 kco
    1781 
    -
    1782 
    -    go swapped substs (TyFamLHS tc tys) ty2 kco
    1783 
    -      = go_fam swapped substs tc tys ty2 kco
    1784 1835
    1785 1836 
         -----------------------------
    1786 
    -    -- go_tv: LHS is a type variable
    1837 
    +    -- LHS is a type variable
    1787 1838 
         -- The sequence of tests is very similar to go_tv
    1788 
    -    go_tv swapped substs tv1 ty2 kco
    1839 
    +    go :: SwapFlag -> UMState -> CanEqLHS -> InType -> OutCoercion -> UM ()
    1840 
    +    go swapped substs lhs@(TyVarLHS tv1) ty2 kco
    1789 1841 
           | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'
    1790 1842 
           = -- We already have a substitution for tv1
    1791 1843 
             if | um_unif env                          -> unify_ty env ty1' ty2 kco
    ... ... @@ -1837,9 +1889,8 @@ uVarOrFam env ty1 ty2 kco
    1837 1889 
           where
    1838 1890 
             tv1'            = umRnOccL env tv1
    1839 1891 
             ty2_fvs         = tyCoVarsOfType ty2
    1840 
    -        rhs_fvs         = ty2_fvs `unionVarSet` tyCoVarsOfCo kco
    1841 1892 
             rhs             = ty2 `mkCastTy` mkSymCo kco
    1842 
    -        tv1_is_bindable | not (tv1' `elemVarSet` um_foralls env)
    1893 
    +        tv1_is_bindable | not (tv1' `elemVarSet` foralld_tvs)
    1843 1894 
                               -- tv1' is not forall-bound, but tv1 can still differ
    1844 1895 
                               -- from tv1; see Note [Cloning the template binders]
    1845 1896 
                               -- in GHC.Core.Rules.  So give tv1' to um_bind_tv_fun.
    ... ... @@ -1848,16 +1899,16 @@ uVarOrFam env ty1 ty2 kco
    1848 1899 
                             | otherwise
    1849 1900 
                             = False
    1850 1901
    1851 
    -        occurs_check = um_unif env &&
    1852 
    -                       occursCheck (um_tv_env substs) tv1 rhs_fvs
    1902 
    +        foralld_tvs  = um_foralls env
    1903 
    +        occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs
    1853 1904 
               -- Occurs check, only when unifying
    1854 1905 
               -- see Note [Infinitary substitutions]
    1855 
    -          -- Make sure you include `kco` in rhs_tvs #14846
    1906 
    +          -- Make sure you include `kco` in rhs #14846
    1856 1907
    1857 1908 
         -----------------------------
    1858 
    -    -- go_fam: LHS is a saturated type-family application
    1909 
    +    -- LHS is a saturated type-family application
    1859 1910 
         -- Invariant: ty2 is not a TyVarTy
    1860 
    -    go_fam swapped substs tc1 tys1 ty2 kco
    1911 
    +    go swapped substs lhs@(TyFamLHS tc1 tys1) ty2 kco
    1861 1912 
           -- If we are under a forall, just give up and return MaybeApart
    1862 1913 
           -- see (ATF3) in Note [Apartness and type families]
    1863 1914 
           | not (isEmptyVarSet (um_foralls env))
    ... ... @@ -1878,14 +1929,17 @@ uVarOrFam env ty1 ty2 kco
    1878 1929 
           -- Check for equality  F tys1 ~ F tys2
    1879 1930 
           | Just (tc2, tys2) <- isSatFamApp ty2
    1880 1931 
           , tc1 == tc2
    1881 
    -      = go_fam_fam tc1 tys1 tys2 kco
    1932 
    +      = go_fam_fam substs tc1 tys1 tys2 kco
    1882 1933
    1883 1934 
           -- Now check if we can bind the (F tys) to the RHS
    1884 1935 
           -- This can happen even when matching: see (ATF7)
    1885 1936 
           | BindMe <- um_bind_fam_fun env tc1 tys1 rhs
    1886 
    -      = -- ToDo: do we need an occurs check here?
    1887 
    -        do { extendFamEnv tc1 tys1 rhs
    1888 
    -           ; maybeApart MARTypeFamily }
    1937 
    +      = if uOccursCheck substs emptyVarSet lhs rhs
    1938 
    +        then maybeApart MARInfinite
    1939 
    +        else do { extendFamEnv tc1 tys1 rhs
    1940 
    +                     -- We don't substitute tys1 before extending
    1941 
    +                     -- See Note [Shortcomings of the apartness test]
    1942 
    +                ; maybeApart MARTypeFamily }
    1889 1943
    1890 1944 
           -- Swap in case of (F a b) ~ (G c d e)
    1891 1945 
           -- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e)
    ... ... @@ -1905,7 +1959,8 @@ uVarOrFam env ty1 ty2 kco
    1905 1959 
         -----------------------------
    1906 1960 
         -- go_fam_fam: LHS and RHS are both saturated type-family applications,
    1907 1961 
         --             for the same type-family F
    1908 
    -    go_fam_fam tc tys1 tys2 kco
    1962 
    +    -- Precondition: um_foralls is empty
    1963 
    +    go_fam_fam substs tc tys1 tys2 kco
    1909 1964 
            -- Decompose (F tys1 ~ F tys2): (ATF9)
    1910 1965 
            -- Use injectivity information of F: (ATF10)
    1911 1966 
            -- But first bind the type-fam if poss: (ATF11)
    ... ... @@ -1925,13 +1980,13 @@ uVarOrFam env ty1 ty2 kco
    1925 1980 
            bind_fam_if_poss
    1926 1981 
              | not (um_unif env)  -- Not when matching (ATF11-1)
    1927 1982 
              = return ()
    1928 
    -         | tcEqTyConAppArgs tys1 tys2   -- Detect (F tys ~ F tys);
    1929 
    -         = return ()                    -- otherwise we'd build an infinite substitution
    1930 1983 
              | BindMe <- um_bind_fam_fun env tc tys1 rhs1
    1931 
    -         = extendFamEnv tc tys1 rhs1
    1932 
    -         | um_unif env
    1933 
    -         , BindMe <- um_bind_fam_fun env tc tys2 rhs2
    1934 
    -         = extendFamEnv tc tys2 rhs2
    1984 
    +         = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $
    1985 
    +           extendFamEnv tc tys1 rhs1
    1986 
    +         -- At this point um_unif=True, so we can unify either way
    1987 
    +         | BindMe <- um_bind_fam_fun env tc tys2 rhs2
    1988 
    +         = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys2) rhs2) $
    1989 
    +           extendFamEnv tc tys2 rhs2
    1935 1990 
              | otherwise
    1936 1991 
              = return ()
    1937 1992
    ... ... @@ -1939,17 +1994,92 @@ uVarOrFam env ty1 ty2 kco
    1939 1994 
            rhs2 = mkTyConApp tc tys1 `mkCastTy` kco
    1940 1995
    1941 1996
    1942 
    -occursCheck :: TvSubstEnv -> TyVar -> TyCoVarSet -> Bool
    1943 
    -occursCheck env tv1 tvs
    1944 
    -  = anyVarSet bad tvs
    1997 
    +uOccursCheck :: UMState
    1998 
    +             -> TyVarSet -- Bound by enclosing foralls; see (OCU1)
    1999 
    +             -> CanEqLHS -> Type   -- Can we unify (lhs := ty)?
    2000 
    +             -> Bool
    2001 
    +-- See Note [The occurs check in the Core unifier] and (ATF13)
    2002 
    +uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) bvs lhs ty
    2003 
    +  = go bvs ty
    1945 2004 
       where
    1946 
    -    bad tv | Just ty <- lookupVarEnv env tv
    1947 
    -           = anyVarSet bad (tyCoVarsOfType ty)
    1948 
    -           | otherwise
    1949 
    -           = tv == tv1
    1950 
    -
    1951 
    -{- Note [Unifying coercion-foralls]
    1952 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2005 
    +    go :: TyCoVarSet   -- Bound by enclosing foralls; see (OCU1)
    2006 
    +       -> Type -> Bool
    2007 
    +    go bvs ty | Just ty' <- coreView ty = go bvs ty'
    2008 
    +    go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv
    2009 
    +                        = go bvs ty'
    2010 
    +                        | TyVarLHS tv' <- lhs, tv==tv'
    2011 
    +                        = True
    2012 
    +                        | otherwise
    2013 
    +                        = go bvs (tyVarKind tv)
    2014 
    +    go bvs (AppTy ty1 ty2)           = go bvs ty1 || go bvs ty2
    2015 
    +    go _   (LitTy {})                = False
    2016 
    +    go bvs (FunTy _ w arg res)       = go bvs w || go bvs arg || go bvs res
    2017 
    +    go bvs (TyConApp tc tys)         = go_tc bvs tc tys
    2018 
    +
    2019 
    +    go bvs (ForAllTy (Bndr tv _) ty)
    2020 
    +      = go bvs (tyVarKind tv) ||
    2021 
    +        (case lhs of
    2022 
    +           TyVarLHS tv' | tv==tv'   -> False  -- Shadowing
    2023 
    +                        | otherwise -> go (bvs `extendVarSet` tv) ty
    2024 
    +           TyFamLHS {} -> False)  -- Lookups don't happen under a forall
    2025 
    +
    2026 
    +    go bvs (CastTy ty  _co) = go bvs ty  -- ToDo: should we worry about `co`?
    2027 
    +    go _   (CoercionTy _co) = False      -- ToDo: should we worry about `co`?
    2028 
    +
    2029 
    +    go_tc bvs tc tys
    2030 
    +      | isEmptyVarSet bvs   -- Never look up in um_fam_env under a forall (ATF3)
    2031 
    +      , isTypeFamilyTyCon tc
    2032 
    +      , Just ty' <- lookupFamEnv fam_env tc (take arity tys)
    2033 
    +             -- NB: we look up /un-substituted/ types;
    2034 
    +             -- See Note [Shortcomings of the apartness test]
    2035 
    +      = go bvs ty' || any (go bvs) (drop arity tys)
    2036 
    +
    2037 
    +      | TyFamLHS tc' tys' <- lhs
    2038 
    +      , tc == tc'
    2039 
    +      , tys `lengthAtLeast` arity  -- Saturated, or over-saturated
    2040 
    +      , tcEqTyConAppArgs tys tys'
    2041 
    +      = True
    2042 
    +
    2043 
    +      | otherwise
    2044 
    +      = any (go bvs) tys
    2045 
    +      where
    2046 
    +        arity = tyConArity tc
    2047 
    +
    2048 
    +{- Note [The occurs check in the Core unifier]
    2049 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    2050 
    +The unifier applies both substitutions (um_tv_env and um_fam_env) as it goes,
    2051 
    +so we'll get an infinite loop if we have, for example
    2052 
    +    um_tv_env:   a :-> F b      -- (1)
    2053 
    +    um_fam_env   F b :-> a      -- (2)
    2054 
    +
    2055 
    +So (uOccursCheck substs lhs ty) returns True iff extending `substs` with `lhs :-> ty`
    2056 
    +could lead to a loop. That is, could there by a type `s` such that
    2057 
    +  applySubsts( (substs + lhs:->ty), s ) is infinite
    2058 
    +
    2059 
    +It's vital that we do both at once: we might have (1) already and add (2);
    2060 
    +or we might have (2) already and add (1).
    2061 
    +
    2062 
    +A very similar task is done by GHC.Tc.Utils.Unify.checkTyEqRhs.
    2063 
    +
    2064 
    +(OCU1) We keep track of the forall-bound variables because the um_fam_env is inactive
    2065 
    +  under a forall; indeed it is /unsound/ to consult it because we may have a binding
    2066 
    +  (F a :-> Int), and then unify (forall a. ...(F a)...) with something.  We don't
    2067 
    +  want to map that (F a) to Int!
    2068 
    +
    2069 
    +(OCU2) Performance. Consider unifying
    2070 
    +         [a, b] ~ [big-ty, (a,a,a)]
    2071 
    +  We'll unify a:=big-ty.  Then we'll attempt b:=(a,a,a), but must do an occurs check.
    2072 
    +  So we'll walk over big-ty, looking for `b`.  And then again, and again, once for
    2073 
    +  each occurrence of `a`.  A similar thing happens for
    2074 
    +         [a, (b,b,b)] ~ [big-ty, (a,a,a)]
    2075 
    +  albeit a bit less obviously.
    2076 
    +
    2077 
    +  Potentially we could use a cache to record checks we have already done;
    2078 
    +  but I have not attempted that yet.  Precisely similar remarks would apply
    2079 
    +  to GHC.Tc.Utils.Unify.checkTyEqRhs
    2080 
    +
    2081 
    +Note [Unifying coercion-foralls]
    2082 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1953 2083 
     Suppose we try to unify (forall cv. t1) ~ (forall cv. t2).
    1954 2084 
     See Note [ForAllTy] in GHC.Core.TyCo.Rep.
    1955 2085

  • compiler/GHC/Tc/Gen/App.hs
    ... ... @@ -430,7 +430,7 @@ tcApp rn_expr exp_res_ty
    430 430 
                              -- Step 5.2: typecheck the arguments, and monomorphise
    431 431 
                              --           any un-unified instantiation variables
    432 432 
                            ; tc_args <- tcValArgs DoQL inst_args
    433 
    -                         -- Step 5.3: zonk to expose the polymophism hidden under
    433 
    +                         -- Step 5.3: zonk to expose the polymorphism hidden under
    434 434 
                              --           QuickLook instantiation variables in `app_res_rho`
    435 435 
                            ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
    436 436 
                              -- Step 5.4: subsumption check against the expected type

  • compiler/GHC/Tc/Types/Evidence.hs
    ... ... @@ -206,9 +206,15 @@ instance Monoid HsWrapper where
    206 206 
     (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
    207 207 
     WpHole    <.> c         = c
    208 208 
     c         <.> WpHole    = c
    209 
    -WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2)
    209 
    +WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
    210 210 
       -- If we can represent the HsWrapper as a cast, try to do so: this may avoid
    211 211 
       -- unnecessary eta-expansion (see 'mkWpFun').
    212 
    +  --
    213 
    +  -- NB: <.> behaves like function composition:
    214 
    +  --
    215 
    +  --   WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
    216 
    +  --
    217 
    +  -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
    212 218 
     c1        <.> c2        = c1 `WpCompose` c2
    213 219
    214 220 
     -- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing

  • compiler/GHC/Tc/Utils/Unify.hs
    ... ... @@ -3342,8 +3342,9 @@ mapCheck f xs
    3342 3342 
     -- | Options describing how to deal with a type equality
    3343 3343 
     -- in the eager unifier. See 'checkTyEqRhs'
    3344 3344 
     data TyEqFlags m a
    3345 
    -  -- | LHS is a type family application; we are not unifying.
    3346 
    -  = TEFTyFam
    3345 
    +  = -- | TFTyFam: LHS is a type family application
    3346 
    +    -- Invariant: we are not unifying; see `notUnifying_TEFTask`
    3347 
    +    TEFTyFam
    3347 3348 
         { tefTyFam_occursCheck :: CheckTyEqProblem
    3348 3349 
            -- ^ The 'CheckTyEqProblem' to report for occurs-check failures
    3349 3350 
            -- (soluble or insoluble)
    ... ... @@ -3352,7 +3353,8 @@ data TyEqFlags m a
    3352 3353 
         , tef_fam_app :: TyEqFamApp m a
    3353 3354 
             -- ^ How to deal with type family applications
    3354 3355 
         }
    3355 
    -  -- | LHS is a 'TyVar'.
    3356 
    +
    3357 
    +  -- | TEFTyVar: LHS is a 'TyVar'.
    3356 3358 
       | TEFTyVar
    3357 3359 
         -- NB: this constructor does not actually store a 'TyVar', in order to
    3358 3360 
         -- support being called from 'makeTypeConcrete' (which works as if we

  • testsuite/tests/typecheck/should_compile/T26346.hs
    1 
    +{-# LANGUAGE GHC2024 #-}
    2 
    +{-# LANGUAGE TypeFamilies #-}
    3 
    +{-# LANGUAGE UndecidableInstances #-}
    4 
    +module T26346 (warble) where
    5 
    +
    6 
    +import Data.Kind (Type)
    7 
    +import Data.Type.Equality ((:~:)(..))
    8 
    +
    9 
    +type Nat :: Type
    10 
    +data Nat = Z | S Nat
    11 
    +
    12 
    +type SNat :: Nat -> Type
    13 
    +data SNat n where
    14 
    +  SZ :: SNat Z
    15 
    +  SS :: SNat n -> SNat (S n)
    16 
    +
    17 
    +type NatPlus :: Nat -> Nat -> Nat
    18 
    +type family NatPlus a b where
    19 
    +  NatPlus Z     b = b
    20 
    +  NatPlus (S a) b = S (NatPlus a b)
    21 
    +
    22 
    +sNatPlus ::
    23 
    +  forall (a :: Nat) (b :: Nat).
    24 
    +  SNat a ->
    25 
    +  SNat b ->
    26 
    +  SNat (NatPlus a b)
    27 
    +sNatPlus SZ     b = b
    28 
    +sNatPlus (SS a) b = SS (sNatPlus a b)
    29 
    +
    30 
    +data Bin
    31 
    +  = Zero
    32 
    +  | Even Bin
    33 
    +  | Odd Bin
    34 
    +
    35 
    +type SBin :: Bin -> Type
    36 
    +data SBin b where
    37 
    +  SZero :: SBin Zero
    38 
    +  SEven :: SBin n -> SBin (Even n)
    39 
    +  SOdd  :: SBin n -> SBin (Odd n)
    40 
    +
    41 
    +type Incr :: Bin -> Bin
    42 
    +type family Incr b where
    43 
    +  Incr Zero     = Odd Zero      -- 0 + 1 = (2*0) + 1
    44 
    +  Incr (Even n) = Odd n         -- 2n + 1
    45 
    +  Incr (Odd n)  = Even (Incr n) -- (2n + 1) + 1 = 2*(n + 1)
    46 
    +
    47 
    +type BinToNat :: Bin -> Nat
    48 
    +type family BinToNat b where
    49 
    +  BinToNat Zero     = Z
    50 
    +  BinToNat (Even n) = NatPlus (BinToNat n) (BinToNat n)
    51 
    +  BinToNat (Odd n)  = S (NatPlus (BinToNat n) (BinToNat n))
    52 
    +
    53 
    +sBinToNat ::
    54 
    +  forall (b :: Bin).
    55 
    +  SBin b ->
    56 
    +  SNat (BinToNat b)
    57 
    +sBinToNat SZero     = SZ
    58 
    +sBinToNat (SEven n) = sNatPlus (sBinToNat n) (sBinToNat n)
    59 
    +sBinToNat (SOdd n)  = SS (sNatPlus (sBinToNat n) (sBinToNat n))
    60 
    +
    61 
    +warble ::
    62 
    +  forall (b :: Bin).
    63 
    +  SBin b ->
    64 
    +  BinToNat (Incr b) :~: S (BinToNat b)
    65 
    +warble SZero = Refl
    66 
    +warble (SEven {}) = Refl
    67 
    +warble (SOdd  sb) | Refl <- warble sb
    68 
    +                  , Refl <- plusComm sbn (SS sbn)
    69 
    +                  = Refl
    70 
    +  where
    71 
    +    sbn = sBinToNat sb
    72 
    +
    73 
    +    plus0R ::
    74 
    +      forall (n :: Nat).
    75 
    +      SNat n ->
    76 
    +      NatPlus n Z :~: n
    77 
    +    plus0R SZ = Refl
    78 
    +    plus0R (SS sn)
    79 
    +      | Refl <- plus0R sn
    80 
    +      = Refl
    81 
    +
    82 
    +    plusSnR ::
    83 
    +      forall (n :: Nat) (m :: Nat).
    84 
    +      SNat n ->
    85 
    +      SNat m ->
    86 
    +      NatPlus n (S m) :~: S (NatPlus n m)
    87 
    +    plusSnR SZ _ = Refl
    88 
    +    plusSnR (SS sn) sm
    89 
    +      | Refl <- plusSnR sn sm
    90 
    +      = Refl
    91 
    +
    92 
    +    plusComm ::
    93 
    +      forall (n :: Nat) (m :: Nat).
    94 
    +      SNat n ->
    95 
    +      SNat m ->
    96 
    +      NatPlus n m :~: NatPlus m n
    97 
    +    plusComm SZ sm
    98 
    +      | Refl <- plus0R sm
    99 
    +      = Refl
    100 
    +    plusComm (SS sn) sm
    101 
    +      | Refl <- plusComm sn sm
    102 
    +      , Refl <- plusSnR sm sn
    103 
    +      = Refl

  • testsuite/tests/typecheck/should_compile/T26350.hs
    1 
    +{-# LANGUAGE DeepSubsumption #-}
    2 
    +{-# LANGUAGE TypeFamilies #-}
    3 
    +{-# LANGUAGE TypeOperators #-}
    4 
    +
    5 
    +{-# OPTIONS_GHC -dcore-lint #-}
    6 
    +
    7 
    +module T26350 where
    8 
    +
    9 
    +import Control.Arrow (first)
    10 
    +
    11 
    +infix 6 .-.
    12 
    +
    13 
    +class AffineSpace p where
    14 
    +  type Diff p
    15 
    +  (.-.) :: p -> p -> Diff p
    16 
    +
    17 
    +affineCombo :: (AffineSpace p, v ~ Diff p) => p -> (p,v) -> (v,v)
    18 
    +affineCombo z l = first (.-. z) l

  • testsuite/tests/typecheck/should_compile/T26358.hs
    1 
    +{-# LANGUAGE TypeFamilies #-}
    2 
    +
    3 
    +module T26358 where
    4 
    +import Data.Kind
    5 
    +import Data.Proxy
    6 
    +
    7 
    +{- Two failing tests, described in GHC.Core.Unify
    8 
    +     Note [Shortcomings of the apartness test]
    9 
    +
    10 
    +Explanation for TF2
    11 
    +* We try to reduce
    12 
    +    (TF2 (F (G Float)) (F Int) (G Float))
    13 
    +* We can only do so if those arguments are apart from the first
    14 
    +  equation of TF2, namely (Bool,Char,Int).
    15 
    +* So we try to unify
    16 
    +    [F (G Float), F Int, G Float] ~ [Bool, Char, Int]
    17 
    +* They really are apart, but we can't quite spot that yet;
    18 
    +  hence #26358
    19 
    +
    20 
    +TF1 is similar.
    21 
    +-}
    22 
    +
    23 
    +
    24 
    +type TF1 :: Type -> Type -> Type -> Type
    25 
    +type family TF1 a b c where
    26 
    +  TF1 Bool Char a = Word
    27 
    +  TF1 a    b    c = (a,b,c)
    28 
    +
    29 
    +type F :: Type -> Type
    30 
    +type family F a where
    31 
    +
    32 
    +foo :: Proxy a
    33 
    +    -> Proxy (TF1 (F a) (F Int) Int)
    34 
    +    -> Proxy (F a, F Int, Int)
    35 
    +foo _ px = px
    36 
    +
    37 
    +type TF2 :: Type -> Type -> Type -> Type
    38 
    +type family TF2 a b c where
    39 
    +  TF2 Bool Char Int = Word
    40 
    +  TF2 a    b    c   = (a,b,c)
    41 
    +
    42 
    +type G :: Type -> Type
    43 
    +type family G a where
    44 
    +
    45 
    +bar :: Proxy (TF2 (F (G Float)) (F Int) (G Float))
    46 
    +    -> Proxy (F (G Float), F Int, G Float)
    47 
    +bar px = px
    48 
    +

  • testsuite/tests/typecheck/should_compile/all.T
    ... ... @@ -862,6 +862,7 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98'])
    862 862 
     test('DeepSubsumption07', normal, compile, ['-XHaskell2010'])
    863 863 
     test('DeepSubsumption08', normal, compile, [''])
    864 864 
     test('DeepSubsumption09', normal, compile, [''])
    865 
    +test('T26350', normal, compile, [''])
    865 866 
     test('T26225', normal, compile, [''])
    866 867 
     test('T26225b', normal, compile, [''])
    867 868 
     test('T21765', normal, compile, [''])
    ... ... @@ -945,3 +946,5 @@ test('T25992', normal, compile, [''])
    945 946 
     test('T14010', normal, compile, [''])
    946 947 
     test('T26256a', normal, compile, [''])
    947 948 
     test('T25992a', normal, compile, [''])
    949 
    +test('T26346', normal, compile, [''])
    950 
    +test('T26358', expect_broken(26358), compile, [''])

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help